Theorem cbvexvw 2038

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2401 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 2037	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 320	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1781	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1781	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  cbvex2vw  2042  mojust  2534  mo4  2561  eujust  2566  cbveuvw  2600  iseqsetvlem  2794  cbvrexvw  3211  euind  3683  reuind  3712  cbvopab1v  5169  cbvopab2v  5170  bm1.3iiOLD  5240  reusv2lem2  5337  relop  5790  dmcoss  5914  dmcossOLD  5915  fv3  6840  exfo  7038  cbvoprab3v  7438  zfun  7669  suppimacnv  8104  frrlem1  8216  ac6sfi  9168  brwdom2  9459  ttrclss  9610  ttrclselem2  9616  aceq1  10005  aceq0  10006  aceq3lem  10008  dfac4  10010  kmlem2  10040  kmlem13  10051  axdc4lem  10343  zfac  10348  zfcndun  10503  zfcndac  10507  sup2  12075  supmul  12091  climmo  15461  summo  15621  prodmo  15840  gsumval3eu  19814  elpt  23485  gsumwrd2dccatlem  33041  1arithidomlem1  33495  1arithidom  33497  bnj1185  34800  axreg  35113  axregscl  35114  tz9.1regs  35118  fineqvac  35127  satf0op  35409  sat1el2xp  35411  cbvrexvw2  36260  cbvoprab1vw  36270  cbvoprab2vw  36271  cbvoprab13vw  36274  bj-bm1.3ii  37097  wl-ax12v2cl  37539  fdc  37784  sn-sup2  42523  cpcoll2d  44291  axc11next  44438  fnchoice  45065  ichexmpl1  47499