Theorem 19.42v 1307

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

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

This theorem is referenced by:  exdistr 1308  19.42vv 1309  3exdistr 1311  4exdistr 1312  2sb5 1334  2sb5rf 1337  r2ex 1689  ceqsex2 1833  sbccomglem 1985  dfiun2g 2582  bm1.3ii 2702  eqvinop 2787  copsexg 2788  uniuni 2876  opelxp 3210  dmopabss 3317  dmopab3 3318  dmsnop 3324  dmcoss 3359  dmcosseq 3361  coass 3508  zfrep6 3610  iinon 3905  dfoprab2 3986  dmoprab 3997  dmoprabss 3998  fnoprabg 4007  2ndconst 4090  fodomfi 4549  rankuni 4681  aceq1 4712  aceq3 4716  ac5b 4736  kmlem14 4761  kmlem15 4762  genpdm 5088  genpn0 5089  distrlem1pr 5110  1idpr 5116  prlem934 5122  ltexprlem1 5125  ltexprlem4 5128  infmap2lem1 7539  bcthlem14 7974  osumlem5 9539  nmcopexlem1 9907  nmcfnexlem1 9936  rcfpfillem3 10513

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977

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

Copyright terms: Public domain