Theorem cbvexvw 2039

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2405 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)

Hypothesis

Ref	Expression
cbvalvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvexvw	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvexvw

Step	Hyp	Ref	Expression
1		cbvalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2038	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 320	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1782	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1782	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1540  ∃wex 1781

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 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  cbvex2vw  2043  mojust  2538  mo4  2566  eujust  2571  cbveuvw  2605  iseqsetvlem  2799  cbvrexvw  3216  euind  3670  reuind  3699  cbvopab1v  5163  cbvopab2v  5164  bm1.3iiOLD  5237  reusv2lem2  5341  axprg  5379  relop  5805  dmcoss  5930  dmcossOLD  5931  fv3  6858  exfo  7057  cbvoprab3v  7459  zfun  7690  suppimacnv  8124  frrlem1  8236  ac6sfi  9194  brwdom2  9488  ttrclss  9641  ttrclselem2  9647  aceq1  10039  aceq0  10040  aceq3lem  10042  dfac4  10044  kmlem2  10074  kmlem13  10085  axdc4lem  10377  zfac  10382  zfcndun  10538  zfcndac  10542  sup2  12112  supmul  12128  climmo  15519  summo  15679  prodmo  15901  gsumval3eu  19879  elpt  23537  gsumwrd2dccatlem  33138  1arithidomlem1  33595  1arithidom  33597  bnj1185  34935  axprALT2  35253  fineqvac  35260  axreg  35271  axregscl  35272  tz9.1regs  35278  satf0op  35559  sat1el2xp  35561  cbvrexvw2  36409  cbvoprab1vw  36419  cbvoprab2vw  36420  cbvoprab13vw  36423  mh-regprimbi  36727  bj-bm1.3ii  37371  wl-ax12v2cl  37822  wl-dfclel  37831  fdc  38066  sn-sup2  42936  cpcoll2d  44686  axc11next  44833  fnchoice  45460  ichexmpl1  47929