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

Theorem cbvexv1 2313
Description: Version of cbvex 2369 with a disjoint variable condition, which does not require ax-13 2334. See cbvexvw 2087 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2371 for another variant. (Contributed by BJ, 31-May-2019.)
Hypotheses
Ref Expression
cbvalv1.nf1 𝑦𝜑
cbvalv1.nf2 𝑥𝜓
cbvalv1.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvexv1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvexv1
StepHypRef Expression
1 cbvalv1.nf1 . . . . 5 𝑦𝜑
21nfn 1902 . . . 4 𝑦 ¬ 𝜑
3 cbvalv1.nf2 . . . . 5 𝑥𝜓
43nfn 1902 . . . 4 𝑥 ¬ 𝜓
5 cbvalv1.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 310 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbvalv1 2312 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 312 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1824 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1824 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 295 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wal 1599  wex 1823  wnf 1827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-11 2150  ax-12 2163
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828
This theorem is referenced by:  sb8ev  2322  exsb  2327  mof  2578  euf  2595  clelab  2916  issetf  3410  eqvincf  3534  rexab2  3583  euabsn  4493  eluniab  4682  cbvopab1  4959  cbvopab2  4960  cbvopab1s  4961  axrep1  5007  axrep2  5009  axrep4  5011  opeliunxp  5416  dfdmf  5562  dfrnf  5610  elrnmpt1  5620  cbvoprab1  7004  cbvoprab2  7005  opabex3d  7423  opabex3  7424  zfcndrep  9771  fsum2dlem  14906  fprod2dlem  15113  bnj1146  31461  bnj607  31585  bnj1228  31678  bj-axrep1  33365  bj-axrep2  33366  bj-axrep4  33368  poimirlem26  34063  sbcexf  34543  elunif  40112  stoweidlem46  41194  opeliun2xp  43130
  Copyright terms: Public domain W3C validator