Theorem 19.41v 1300

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

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

This theorem is referenced by:  19.41vv 1301  19.41vvv 1302  eeeanv 1319  r19.41v 1755  gencbvex 1829  euxfr 1917  sbcgf 1976  iunconst 2562  zfpair 2767  opabid 2799  opabn0 2813  opelxp 3204  relop 3265  dmuni 3308  dmres 3364  rnuni 3445  dminss 3448  imainss 3449  ssrnres 3467  resco 3486  rnco 3488  coass 3498  f11o 3697  imaiun 3849  rnoprab 3989  domen 4361  xpassen 4421  kmlem3 4739  cflem 4877  prnmadd 5072  genpass 5084  ltexprlem4 5117  reclem1pr 5128  reclem2pr 5129  suplem1pr 5133  elreal 5222  infcvglem1 7156  19.41vvvv 10335  eeeeanv 10336

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain