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

Theorem cbvexv1 2364
 Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2419 with a disjoint variable condition, which does not require ax-13 2392. See cbvexvw 2045 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2421 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised 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 1858 . . . 4 𝑦 ¬ 𝜑
3 cbvalv1.nf2 . . . . 5 𝑥𝜓
43nfn 1858 . . . 4 𝑥 ¬ 𝜓
5 cbvalv1.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 321 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbvalv1 2363 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
87notbii 323 . 2 (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
9 df-ex 1782 . 2 (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
10 df-ex 1782 . 2 (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
118, 9, 103bitr4i 306 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-11 2162  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786 This theorem is referenced by:  sb8ev  2376  exsb  2380  mof  2648  euf  2662  cbveuw  2692  clelab  2959  issetf  3493  eqvincf  3629  rexab2  3677  rexab2OLD  3678  euabsn  4647  eluniab  4839  cbvopab1  5125  cbvopab1g  5126  cbvopab2  5127  cbvopab1s  5128  axrep1  5177  axrep2  5179  axrep4  5181  opeliunxp  5606  dfdmf  5752  dfrnf  5807  elrnmpt1  5817  cbvoprab1  7234  cbvoprab2  7235  opabex3d  7661  opabex3rd  7662  opabex3  7663  zfcndrep  10034  fsum2dlem  15125  fprod2dlem  15334  bnj1146  32120  bnj607  32245  bnj1228  32340  poimirlem26  35028  sbcexf  35498  elunif  41565  stoweidlem46  42614  opeliun2xp  44660
 Copyright terms: Public domain W3C validator