Theorem hbel 1566

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

Hypotheses

Ref	Expression
hbel.1	|- (y e. A -> A.x y e. A)
hbel.2	|- (z e. B -> A.x z e. B)

Assertion

Ref	Expression
hbel	|- (A e. B -> A.x A e. B)

Distinct variable groups:   y,A   z,B   x,y   x,z

Proof of Theorem hbel

Step	Hyp	Ref	Expression
1		ax-17 971	. . . . 5 |- (y e. w -> A.x y e. w)
2		hbel.1	. . . . 5 |- (y e. A -> A.x y e. A)
3	1, 2	hbeq 1565	. . . 4 |- (w = A -> A.x w = A)
4		hbel.2	. . . . 5 |- (z e. B -> A.x z e. B)
5	4	hblem 1564	. . . 4 |- (w e. B -> A.x w e. B)
6	3, 5	hban 1009	. . 3 |- ((w = A /\ w e. B) -> A.x(w = A /\ w e. B))
7	6	hbex 1006	. 2 |- (E.w(w = A /\ w e. B) -> A.xE.w(w = A /\ w e. B))
8		df-clel 1472	. 2 |- (A e. B <-> E.w(w = A /\ w e. B))
9	8	albii 999	. 2 |- (A.x A e. B <-> A.xE.w(w = A /\ w e. B))
10	7, 8, 9	3imtr4 219	1 |- (A e. B -> A.x A e. B)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980

This theorem is referenced by:  hbeleq 1567  sbabel 1584  hbrab 1773  cbvralf 1796  cbvrexf 1797  vtoclgaf 1851  elabgt 1895  elabf 1896  elabgf 1898  elrabf 1904  cbvrab 1910  hbeld 1914  hbsbc1 1949  sbcabel 1996  hbcsb1g 2024  hbcsbg 2026  hbif 2373  hbpw 2407  hbuni 2509  hbint 2543  hbbr 2658  opabsb 2815  reuuni2f 2883  reucl 2885  rabxfr 2902  reuunixfr 2906  onminex 3020  hbxp 3204  dfdmf 3306  dfrnf 3348  hbrn 3351  hbima 3411  cnvopab 3445  fnopabg 3615  tz6.12f 3738  fvopab5 3793  ffnfvf 3829  hbiso 3892  foprab2 4119  tz9.12lem3 4661  rankid 4672  rankuni2 4690  scottex 4716  hta 4728  nnwof 6459  isumnn0nna 7208  isummulc1a 7214  isumcmpi 7215

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain