Theorem hbex 1006

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 1004	. . . 4 |- (-. ph -> A.x -. ph)
3	2	hbal 1005	. . 3 |- (A.y -. ph -> A.xA.y -. ph)
4	3	hbn 1004	. 2 |- (-. A.y -. ph -> A.x -. A.y -. ph)
5		df-ex 981	. 2 |- (E.yph <-> -. A.y -. ph)
6	5	albii 999	. 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 954  E.wex 980

This theorem is referenced by:  excomim 1045  19.12 1047  eeor 1120  cbvex2 1317  eeanv 1323  sb7f 1341  hbeu1 1388  hbeu 1389  hbmo 1407  moexex 1438  hbel 1566  hbrex 1688  ceqsex2 1836  hbuni 2509  cbvopab1 2674  cbvopab1s 2675  axrep1 2694  axrep2 2695  axrep3 2696  axrep4 2697  copsex2g 2793  mosubopt 2804  opabid 2810  hbopab 2812  hbopab2 2814  hbxp 3204  hbco 3287  hbcnv 3295  dfdmf 3306  dfrnf 3348  hbrn 3351  hbima 3411  fv3 3733  hboprab2 3994  cbvoprab12 3998  aceq1 4729  zfcndrep 4966  zfcndinf 4970  hbsum1 6983  hbsum 6984

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-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain