Theorem hbex 701

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	hbne 699	. . . 4 |- (-. ph -> A.x -. ph)
3	2	hbal 700	. . 3 |- (A.y -. ph -> A.xA.y -. ph)
4	3	hbne 699	. 2 |- (-. A.y -. ph -> A.x -. A.y -. ph)
5		df-ex 679	. 2 |- (E.yph <-> -. A.y -. ph)
6	5	bial 695	. 2 |- (A.xE.yph <-> A.x -. A.y -. ph)
7	4, 5, 6	3imtr4 192	1 |- (E.yph -> A.xE.yph)

Syntax hints:  -. wn 1   -> wi 2  A.wal 672  E.wex 678

This theorem is referenced by:  excomim 727  19.12 729  eeor 795  cbvex2 975  eeanv 980  hbeu1 1015  hbeu 1016  hbmo 1033  moexex 1058  hbel 1172  hbrex 1238  axrep 1473  axrep2 1474  zfrep2 1475  copsex2g 1903  mosubop 1911  hbuni 1925  opabid 2099  cbvopab1 2106  cbvopab1s 2107  hbopab 2111  hbopab2 2113  hbxp 2444  hbco 2508  hbcnv 2516  dfdmf 2526  dfrnf 2561  hbrn 2564  hbima 2609  fv3 2839  hboprab2 3024  cbvoprab12 3028  aceq1 3552  zfcndrep 3760  zfcndinf 3764

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org