Theorem hbel 1563

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 969	. . . . 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 1562	. . . 4 |- (w = A -> A.x w = A)
4		hbel.2	. . . . 5 |- (z e. B -> A.x z e. B)
5	4	hblem 1561	. . . 4 |- (w e. B -> A.x w e. B)
6	3, 5	hban 1007	. . 3 |- ((w = A /\ w e. B) -> A.x(w = A /\ w e. B))
7	6	hbex 1004	. 2 |- (E.w(w = A /\ w e. B) -> A.xE.w(w = A /\ w e. B))
8		df-clel 1470	. 2 |- (A e. B <-> E.w(w = A /\ w e. B))
9	8	albii 997	. 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 952   = wceq 954   e. wcel 956  E.wex 978

This theorem is referenced by:  hbeleq 1564  sbabel 1581  hbrab 1770  cbvralf 1793  vtoclgaf 1847  elabgt 1891  elabf 1892  elabgf 1894  elrabf 1900  cbvrab 1906  hbeld 1910  hbsbc1 1945  sbcabel 1992  hbcsb1g 2020  hbcsbg 2022  hbif 2369  hbpw 2403  hbuni 2504  hbint 2538  hbbr 2653  opabsb 2810  reuuni2f 2878  reucl 2880  rabxfr 2897  reuunixfr 2901  onminex 3015  hbxp 3199  dfdmf 3301  dfrnf 3342  hbrn 3345  hbima 3403  cnvopab 3437  fnopabg 3607  tz6.12f 3729  fvopab5 3784  ffnfvf 3820  hbiso 3883  foprab2 4109  tz9.12lem3 4641  rankid 4652  rankuni2 4670  scottex 4696  hta 4708  nnwof 6399  isumnn0nna 7151  isummulc1a 7157  isumcmpi 7158  cbvrexf 10374

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain