Theorem 19.41v 1347

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

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

This theorem is referenced by:  19.41vv 1348  19.41vvv 1349  eeeanv 1366  r19.41v 1810  gencbvex 1885  euxfr 1974  sbcgf 2036  iunconst 2626  zfpair 2833  opabid 2866  opabn0 2880  opelxp 3271  relop 3332  dmuni 3376  dmres 3437  rnuni 3516  dminss 3519  imainss 3520  ssrnres 3538  resco 3557  rnco 3559  coass 3569  f11o 3769  imaiun 3921  rnoprab 4062  domen 4440  xpassen 4504  kmlem3 4829  cflem 4970  prnmadd 5165  genpass 5177  ltexprlem4 5210  reclem1pr 5221  reclem2pr 5222  suplem1pr 5226  elreal 5315  infcvglem1 7311  19.41vvvv 10521  eeeeanv 10522

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