Theorem 19.42v 1303

Description: Special case of Theorem 19.42 of [Margaris] p. 90.

Assertion

Ref	Expression
19.42v	|- (E.x(ph /\ ps) <-> (ph /\ E.xps))

Distinct variable group:   ph,x

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2	1	19.42 1092	1 |- (E.x(ph /\ ps) <-> (ph /\ E.xps))

Syntax hints:   <-> wb 146   /\ wa 223  E.wex 977

This theorem is referenced by:  exdistr 1304  19.42vv 1305  3exdistr 1307  4exdistr 1308  2sb5 1330  2sb5rf 1333  r2ex 1683  ceqsex2 1827  sbccomglem 1978  dfiun2g 2576  bm1.3ii 2696  eqvinop 2781  copsexg 2782  uniuni 2870  opelxp 3204  dmopabss 3310  dmopab3 3311  dmsnop 3317  dmcoss 3347  dmcosseq 3349  coass 3498  zfrep6 3600  iinon 3895  dfoprab2 3976  dmoprab 3987  dmoprabss 3988  fnoprabg 3997  2ndconst 4081  fodomfi 4540  rankuni 4670  aceq1 4701  aceq3 4705  ac5b 4725  kmlem14 4750  kmlem15 4751  genpdm 5077  genpn0 5078  distrlem1pr 5099  1idpr 5105  prlem934 5111  ltexprlem1 5114  ltexprlem4 5117  infmap2lem1 7521  bcthlem14 7946  osumlem5 9499  nmcopexlem1 9866  nmcfnexlem1 9895

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978

Copyright terms: Public domain