Theorem 19.41v 1303

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

Assertion

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

Distinct variable group:   ps,x

Proof of Theorem 19.41v

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

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

This theorem is referenced by:  19.41vv 1304  19.41vvv 1305  eeeanv 1322  r19.41v 1760  gencbvex 1834  euxfr 1923  sbcgf 1982  iunconst 2567  zfpair 2772  opabid 2805  opabn0 2819  opelxp 3209  relop 3270  dmuni 3314  dmres 3372  rnuni 3451  dminss 3454  imainss 3455  ssrnres 3473  resco 3492  rnco 3494  coass 3504  f11o 3703  imaiun 3855  rnoprab 3995  domen 4367  xpassen 4427  kmlem3 4747  cflem 4885  prnmadd 5080  genpass 5092  ltexprlem4 5125  reclem1pr 5136  reclem2pr 5137  suplem1pr 5141  elreal 5230  infcvglem1 7164  19.41vvvv 10371  eeeeanv 10372

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain