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

Theorem cbvexv1 2343
Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2402 with a disjoint variable condition, which does not require ax-13 2375. See cbvexvw 2034 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2404 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 1855 . . . 4 𝑦 ¬ 𝜑
3 cbvalv1.nf2 . . . . 5 𝑥𝜓
43nfn 1855 . . . 4 𝑥 ¬ 𝜓
5 cbvalv1.1 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
65notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
72, 4, 6cbvalv1 2342 . . 3 (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8 alnex 1778 . . 3 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9 alnex 1778 . . 3 (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
107, 8, 93bitr3i 301 . 2 (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
1110con4bii 321 1 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1535  wex 1776  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-11 2155  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781
This theorem is referenced by:  sb8ef  2356  exsb  2360  mof  2561  euf  2574  cbveuw  2604  eqvincf  3650  rexab2  3708  euabsn  4731  eluniab  4926  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  axrep1  5286  axrep2  5288  axrep4OLD  5292  opeliunxp  5756  dfdmf  5910  dfrnf  5964  elrnmpt1  5974  cbvoprab1  7520  cbvoprab2  7521  opabex3d  7989  opabex3rd  7990  opabex3  7991  zfcndrep  10652  fsum2dlem  15803  fprod2dlem  16013  2ndresdju  32666  bnj1146  34784  bnj607  34909  bnj1228  35004  fineqvrep  35088  poimirlem26  37633  sbcexf  38102  elunif  44954  stoweidlem46  46002  opeliun2xp  48178
  Copyright terms: Public domain W3C validator