Theorem hbel 1564

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 970	. . . . 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 1563	. . . 4 |- (w = A -> A.x w = A)
4		hbel.2	. . . . 5 |- (z e. B -> A.x z e. B)
5	4	hblem 1562	. . . 4 |- (w e. B -> A.x w e. B)
6	3, 5	hban 1008	. . 3 |- ((w = A /\ w e. B) -> A.x(w = A /\ w e. B))
7	6	hbex 1005	. 2 |- (E.w(w = A /\ w e. B) -> A.xE.w(w = A /\ w e. B))
8		df-clel 1471	. 2 |- (A e. B <-> E.w(w = A /\ w e. B))
9	8	albii 998	. 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 953   = wceq 955   e. wcel 957  E.wex 979

This theorem is referenced by:  hbeleq 1565  sbabel 1582  hbrab 1771  cbvralf 1794  vtoclgaf 1848  elabgt 1892  elabf 1893  elabgf 1895  elrabf 1901  cbvrab 1907  hbeld 1911  hbsbc1 1946  sbcabel 1993  hbcsb1g 2021  hbcsbg 2023  hbif 2370  hbpw 2404  hbuni 2505  hbint 2539  hbbr 2654  opabsb 2811  reuuni2f 2879  reucl 2881  rabxfr 2898  reuunixfr 2902  onminex 3016  hbxp 3200  dfdmf 3302  dfrnf 3344  hbrn 3347  hbima 3407  cnvopab 3441  fnopabg 3611  tz6.12f 3733  fvopab5 3788  ffnfvf 3824  hbiso 3887  foprab2 4112  tz9.12lem3 4644  rankid 4655  rankuni2 4673  scottex 4699  hta 4711  nnwof 6404  isumnn0nna 7160  isummulc1a 7166  isumcmpi 7167  cbvrexf 10396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-cleq 1468  df-clel 1471

Copyright terms: Public domain