Theorem hbel 1172

Description: If x is effectively bound in A and B, it is effectively bound in A ∈ B.

Hypotheses

Ref	Expression
hbel.1	⊢ (y ∈ A → ∀x y ∈ A)
hbel.2	⊢ (z ∈ B → ∀x z ∈ B)

Assertion

Ref	Expression
hbel	⊢ (A ∈ B → ∀x A ∈ B)

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

Proof of Theorem hbel

Step	Hyp	Ref	Expression
1		ax-17 925	. . . . 5 ⊢ (y ∈ w → ∀x y ∈ w)
2		hbel.1	. . . . 5 ⊢ (y ∈ A → ∀x y ∈ A)
3	1, 2	hbeq 1171	. . . 4 ⊢ (w = A → ∀x w = A)
4		hbel.2	. . . . 5 ⊢ (z ∈ B → ∀x z ∈ B)
5	4	hblem 1170	. . . 4 ⊢ (w ∈ B → ∀x w ∈ B)
6	3, 5	hban 704	. . 3 ⊢ ((w = A ∧ w ∈ B) → ∀x(w = A ∧ w ∈ B))
7	6	hbex 701	. 2 ⊢ (∃w(w = A ∧ w ∈ B) → ∀x∃w(w = A ∧ w ∈ B))
8		df-clel 1099	. 2 ⊢ (A ∈ B ↔ ∃w(w = A ∧ w ∈ B))
9	8	bial 695	. 2 ⊢ (∀x A ∈ B ↔ ∀x∃w(w = A ∧ w ∈ B))
10	7, 8, 9	3imtr4 192	1 ⊢ (A ∈ B → ∀x A ∈ B)

Syntax hints:   → wi 2   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  hbeleq 1173  sbabel 1189  hbrab 1311  cbvralf 1330  elabf 1414  elabgf 1416  elrabf 1421  cbvrab 1425  hbsbc 1446  hbpw 1804  hbuni 1925  reucl 1957  hbint 1975  hbbr 2095  opabsb 2114  opelopabg 2115  onminex 2275  hbxp 2444  dfdmf 2526  dfrnf 2561  hbrn 2564  hbima 2609  cnvopab 2632  fnopabg 2745  tz6.12f 2844  hbiso 2930  tz9.12lem3 3505  rankid 3516  rankuni 3533  scottex 3541  hta 3619  nnwof 4609

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