Theorem 19.42v 1308

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

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

This theorem is referenced by:  exdistr 1309  19.42vv 1310  3exdistr 1312  4exdistr 1313  2sb5 1335  2sb5rf 1338  r2ex 1691  ceqsex2 1836  sbccomglem 1988  dfiun2g 2586  bm1.3ii 2706  eqvinop 2791  copsexg 2792  uniuni 2880  opelxp 3214  dmopabss 3321  dmopab3 3322  dmsnop 3328  dmcoss 3363  dmcosseq 3365  coass 3512  zfrep6 3614  iinon 3910  dfoprab2 3991  dmoprab 4002  dmoprabss 4003  fnoprabg 4012  2ndconst 4097  fodomfiOLD 4566  rankuni 4698  aceq1 4729  aceq3 4733  ac5b 4753  kmlem14 4778  kmlem15 4779  genpdm 5105  genpn0 5106  distrlem1pr 5127  1idpr 5133  prlem934 5139  ltexprlem1 5142  ltexprlem4 5145  infmap2lem1 7579  bcthlem14 8012  osumlem5 9582  nmcopexlem1 9951  nmcfnexlem1 9980  rcfpfillem3 10589  rcfpfillem3OLD 10590

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain