Theorem hbeleq 1173

Description: If x is effectively bound in y ∈ A, then it is effectively bound in y = A.

Hypothesis

Ref	Expression
hbeleq.1	⊢ (y ∈ A → ∀x y ∈ A)

Assertion

Ref	Expression
hbeleq	⊢ (y = A → ∀x y = A)

Distinct variable group(s):   x,y   y,A

Proof of Theorem hbeleq

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (z ∈ y → ∀x z ∈ y)
2		ax-17 925	. . 3 ⊢ (y ∈ z → ∀x y ∈ z)
3		hbeleq.1	. . 3 ⊢ (y ∈ A → ∀x y ∈ A)
4	2, 3	hbel 1172	. 2 ⊢ (z ∈ A → ∀x z ∈ A)
5	1, 4	hbeq 1171	1 ⊢ (y = A → ∀x y = A)

Syntax hints:   → wi 2  ∀wal 672   ∈ wel 803   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  vtoclgf 1382  cla4gf 1394  eqvincf 1408  hbpr 1824  hbsuc 2294  zfrep6 2744  fvopabgf 2874  fvopabnf 2875  oprabval4g 3053  mapxpen 3390  xpmapenlem1 3391  xpmapenlem4 3394  tz9.12lem3 3505  scott0 3542  cplem2 3546  ac6lem 3575  seqlem1 4662

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-9 799  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org