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

Theorem cbvexv1 2353
Description: Version of cbvex 2408 with a disjoint variable condition, which does not require ax-13 2381. See cbvexvw 2035 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2410 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 1848 . . . 4 𝑦 ¬ 𝜑
3 cbvalv1.nf2 . . . . 5 𝑥𝜓
43nfn 1848 . . . 4 𝑥 ¬ 𝜓
5 cbvalv1.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 319 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbvalv1 2352 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 321 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1772 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1772 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 304 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wal 1526  wex 1771  wnf 1775
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  ax-6 1961  ax-7 2006  ax-11 2151  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776
This theorem is referenced by:  sb8ev  2365  exsb  2369  mof  2640  euf  2654  clelab  2955  issetf  3505  eqvincf  3640  rexab2  3688  rexab2OLD  3689  euabsn  4654  eluniab  4841  cbvopab1  5130  cbvopab1g  5131  cbvopab2  5132  cbvopab1s  5133  axrep1  5182  axrep2  5184  axrep4  5186  opeliunxp  5612  dfdmf  5758  dfrnf  5813  elrnmpt1  5823  cbvoprab1  7230  cbvoprab2  7231  opabex3d  7655  opabex3rd  7656  opabex3  7657  zfcndrep  10024  fsum2dlem  15113  fprod2dlem  15322  bnj1146  31962  bnj607  32087  bnj1228  32180  poimirlem26  34799  sbcexf  35274  elunif  41150  stoweidlem46  42208  opeliun2xp  44309
  Copyright terms: Public domain W3C validator