Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.42v Structured version   Visualization version   GIF version

Theorem 19.42v 1947
 Description: Version of 19.42 2230 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.42v (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v
StepHypRef Expression
1 19.41v 1943 . 2 (∃𝑥(𝜓𝜑) ↔ (∃𝑥𝜓𝜑))
2 exancom 1854 . 2 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
3 ancom 463 . 2 ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓𝜑))
41, 2, 33bitr4i 305 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774 This theorem is referenced by:  exdistr  1948  19.42vv  1951  19.42vvv  1953  19.42vvvOLD  1954  4exdistr  1956  2sb5  2275  eeeanv  2364  eu6lem  2652  rexcom4  3247  rexcom4a  3249  cbvrexdva2  3456  ceqsex2  3542  ceqsex2v  3543  reuind  3742  2reu5lem3  3746  sbccomlem  3851  bm1.3ii  5197  eqvinop  5369  dmopabss  5780  dmopab3  5781  dmres  5868  ssrnres  6028  mptpreima  6085  resco  6096  mptfnf  6476  brprcneu  6655  fndmin  6808  fliftf  7060  dfoprab2  7204  dmoprab  7247  dmoprabss  7248  fnoprabg  7267  uniuni  7476  zfrep6  7648  opabex3d  7658  opabex3rd  7659  opabex3  7660  fsplit  7804  fsplitOLD  7805  eroveu  8384  rankuni  9284  aceq1  9535  dfac3  9539  kmlem14  9581  kmlem15  9582  axdc2lem  9862  1idpr  10443  ltexprlem1  10450  ltexprlem4  10453  xpcogend  14326  shftdm  14422  joindm  17605  meetdm  17619  toprntopon  21525  ntreq0  21677  cnextf  22666  adjeu  29658  rexunirn  30248  fpwrelmapffslem  30460  tgoldbachgt  31922  bnj1019  32039  bnj1209  32056  bnj1033  32229  bnj1189  32269  satfdm  32604  dmscut  33260  dfiota3  33372  brimg  33386  funpartlem  33391  bj-eeanvw  34035  bj-snsetex  34263  bj-snglc  34269  bj-bm1.3ii  34344  bj-restuni  34375  itg2addnc  34933  sbccom2lem  35389  eldmres  35517  rnxrn  35633  rp-isfinite6  39869  undmrnresiss  39949  elintima  39983  pm11.58  40707  pm11.71  40714  2sbc5g  40733  iotasbc2  40737  ax6e2nd  40877  ax6e2ndVD  41227  ax6e2ndALT  41249  stoweidlem60  42330  elpglem3  44800
 Copyright terms: Public domain W3C validator