Theorem hbex 1004

Description: If x is not free in ph, it is not free in E.yph.

Hypothesis

Ref	Expression
hb.1	|- (ph -> A.xph)

Assertion

Ref	Expression
hbex	|- (E.yph -> A.xE.yph)

Proof of Theorem hbex

Step	Hyp	Ref	Expression
1		hb.1	. . . . 5 |- (ph -> A.xph)
2	1	hbn 1002	. . . 4 |- (-. ph -> A.x -. ph)
3	2	hbal 1003	. . 3 |- (A.y -. ph -> A.xA.y -. ph)
4	3	hbn 1002	. 2 |- (-. A.y -. ph -> A.x -. A.y -. ph)
5		df-ex 979	. 2 |- (E.yph <-> -. A.y -. ph)
6	5	albii 997	. 2 |- (A.xE.yph <-> A.x -. A.y -. ph)
7	4, 5, 6	3imtr4 219	1 |- (E.yph -> A.xE.yph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 952  E.wex 978

This theorem is referenced by:  excomim 1043  19.12 1045  eeor 1118  cbvex2 1315  eeanv 1321  sb7f 1339  hbeu1 1386  hbeu 1387  hbmo 1405  moexex 1436  hbel 1563  hbrex 1685  ceqsex2 1832  hbuni 2504  cbvopab1 2669  cbvopab1s 2670  axrep1 2689  axrep2 2690  axrep3 2691  axrep4 2692  copsex2g 2788  mosubopt 2799  opabid 2805  hbopab 2807  hbopab2 2809  hbxp 3199  hbco 3282  hbcnv 3290  dfdmf 3301  dfrnf 3342  hbrn 3345  hbima 3403  fv3 3724  hboprab2 3985  cbvoprab12 3989  aceq1 4709  zfcndrep 4946  zfcndinf 4950  hbsum1 6929  hbsum 6930

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-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain