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

Theorem r19.41v 3344
Description: Restricted quantifier version 19.41v 1941. Version of r19.41 3345 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
Assertion
Ref Expression
r19.41v (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.41v
StepHypRef Expression
1 anass 469 . . . 4 (((𝑥𝐴𝜑) ∧ 𝜓) ↔ (𝑥𝐴 ∧ (𝜑𝜓)))
21exbii 1839 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
3 19.41v 1941 . . 3 (∃𝑥((𝑥𝐴𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
42, 3bitr3i 278 . 2 (∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
5 df-rex 3141 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥(𝑥𝐴 ∧ (𝜑𝜓)))
6 df-rex 3141 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
76anbi1i 623 . 2 ((∃𝑥𝐴 𝜑𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ 𝜓))
84, 5, 73bitr4i 304 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wex 1771  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-rex 3141
This theorem is referenced by:  r19.41vv  3346  r19.42v  3347  3reeanv  3366  reuxfr1d  3738  reuind  3741  iuncom4  4918  dfiun2g  4946  dfiun2gOLD  4947  iunxiun  5010  inuni  5237  xpiundi  5615  xpiundir  5616  imaco  6097  coiun  6102  abrexco  6994  imaiun  6995  isomin  7079  isoini  7080  oarec  8177  mapsnend  8576  genpass  10419  4fvwrd4  13015  4sqlem12  16280  imasleval  16802  lsmspsn  19785  utoptop  22770  metrest  23061  metust  23095  cfilucfil  23096  metuel2  23102  istrkg2ld  26173  axsegcon  26640  fusgreg2wsp  28042  nmoo0  28495  nmop0  29690  nmfn0  29691  rexunirn  30183  dmrab  30187  iunrnmptss  30245  ordtconnlem1  31066  dya2icoseg2  31435  dya2iocnei  31439  omssubaddlem  31456  omssubadd  31457  satfvsuclem2  32504  satf0  32516  satffunlem1lem2  32547  satffunlem2lem2  32550  bj-mpomptALT  34303  mptsnunlem  34501  fvineqsneq  34575  rabiun  34746  iundif1  34747  poimir  34806  ismblfin  34814  eldmqs1cossres  35773  erim2  35791  prter2  35897  prter3  35898  islshpat  36033  lshpsmreu  36125  islpln5  36551  islvol5  36595  cdlemftr3  37581  dvhb1dimN  38002  dib1dim  38181  mapdpglem3  38691  hdmapglem7a  38943  diophrex  39250
  Copyright terms: Public domain W3C validator