Theorem 19.42v 1350

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 1012	. 2 |- (ph -> A.xph)
2	1	19.42 1137	1 |- (E.x(ph /\ ps) <-> (ph /\ E.xps))

Syntax hints:   <-> wb 153   /\ wa 230  E.wex 1021

This theorem is referenced by:  exdistr 1351  19.42vv 1352  3exdistr 1354  4exdistr 1355  2sb5 1377  2sb5rf 1380  r2ex 1738  ceqsex2 1883  sbccomglem 2038  dfiun2g 2640  bm1.3ii 2761  eqvinop 2847  copsexg 2848  uniuni 2937  opelxp 3271  dmopabss 3378  dmopab3 3379  dmsnop 3385  dmcoss 3420  dmcosseq 3422  coass 3569  zfrep6 3671  iinon 3968  dfoprab2 4049  dmoprab 4060  dmoprabss 4061  fnoprabg 4070  2ndconst 4155  fodomfi 4626  rankuni 4760  aceq1 4791  aceq3 4795  ac5b 4815  kmlem14 4840  kmlem15 4841  genpdm 5170  genpn0 5171  distrlem1pr 5192  1idpr 5198  prlem934 5204  ltexprlem1 5207  ltexprlem4 5210  infmap2lem1 7671  bcthlem14 8097  osumlem5 9665  nmcopexlem1 10034  nmcfnexlem1 10063  rcfpfillem3 10673

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022

Copyright terms: Public domain