Theorem 19.41v 1685

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

Syntax hints:   <-> wb 163   /\ wa 240  E.wex 1326

This theorem is referenced by:  19.41vv 1686  19.41vvv 1687  eeeanv 1708  eeeanvOLD 1709  gencbvex 2334  gencbvexOLD 2335  euxfr 2438  euind 2439  sbcgfOLD 2521  iunconstOLD 3263  zfpair 3522  opabidOLD 3558  opabn0 3575  opelxpOLD 4037  relop 4113  dmuni 4166  dmres 4234  rnuni 4327  dminss 4330  imainss 4331  ssrnres 4354  resco 4402  rnco 4404  coass 4415  f11o 4666  imaiun 4840  rnoprab 4933  domen 5438  xpassen 5500  kmlem3 5929  cflem 6053  prnmadd 6252  genpass 6264  ltexprlem4 6297  reclem1pr 6308  reclem2pr 6309  suplem1pr 6313  elreal 6402  infcvglem1 8482  extbas1 10291  bnj512 12519  bnj534 12531  bnj851 12786  bnj903 12819  bnj607 13304  bnj908 13329  bnj986 13360  dftr6 13834  frxp 13951  19.41vvvv 14271  eeeeanv 14272  cnvresima 15359  prter2 16285  prter3 16286  pm11.6 16349  pm11.71 16354

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain