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

Theorem cbvexv1 2344
Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2404 with a disjoint variable condition, which does not require ax-13 2377. See cbvexvw 2036 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2406 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 1857 . . . 4 𝑦 ¬ 𝜑
3 cbvalv1.nf2 . . . . 5 𝑥𝜓
43nfn 1857 . . . 4 𝑥 ¬ 𝜓
5 cbvalv1.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbvalv1 2343 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8 alnex 1781 . . 3 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9 alnex 1781 . . 3 (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
107, 8, 93bitr3i 301 . 2 (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
1110con4bii 321 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1538  wex 1779  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  sb8ef  2358  exsb  2362  mof  2563  euf  2576  cbveuw  2606  eqvincf  3650  rexab2  3705  euabsn  4726  eluniab  4921  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  axrep1  5280  axrep2  5282  axrep4OLD  5286  opeliunxp  5752  opeliun2xp  5753  dfdmf  5907  dfrnf  5961  elrnmpt1  5971  cbvoprab1  7520  cbvoprab2  7521  opabex3d  7990  opabex3rd  7991  opabex3  7992  zfcndrep  10654  fsum2dlem  15806  fprod2dlem  16016  2ndresdju  32659  bnj1146  34805  bnj607  34930  bnj1228  35025  fineqvrep  35109  poimirlem26  37653  sbcexf  38122  elunif  45021  stoweidlem46  46061
  Copyright terms: Public domain W3C validator