Theorem 19.41v 1305

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

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

This theorem is referenced by:  19.41vv 1306  19.41vvv 1307  eeeanv 1324  r19.41v 1762  gencbvex 1836  euxfr 1925  sbcgf 1984  iunconst 2570  zfpair 2775  opabid 2808  opabn0 2822  opelxp 3212  relop 3273  dmuni 3317  dmres 3378  rnuni 3457  dminss 3460  imainss 3461  ssrnres 3479  resco 3498  rnco 3500  coass 3510  f11o 3710  imaiun 3862  rnoprab 4002  domen 4375  xpassen 4435  kmlem3 4755  cflem 4893  prnmadd 5088  genpass 5100  ltexprlem4 5133  reclem1pr 5144  reclem2pr 5145  suplem1pr 5149  elreal 5238  infcvglem1 7179  19.41vvvv 10389  eeeeanv 10390

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