Theorem cbvexvw 2037

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

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

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 2008

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

This theorem is referenced by:  cbvex2vw  2041  mojust  2532  mo4  2559  eujust  2564  cbveuvw  2598  iseqsetvlem  2792  cbvrexvw  3208  cbvrexdva2OLD  3314  euind  3686  reuind  3715  cbvopab1v  5173  cbvopab2v  5174  bm1.3iiOLD  5244  reusv2lem2  5341  relop  5797  dmcoss  5920  dmcossOLD  5921  fv3  6844  exfo  7043  cbvoprab3v  7445  zfun  7676  suppimacnv  8114  frrlem1  8226  ac6sfi  9189  brwdom2  9484  ttrclss  9635  ttrclselem2  9641  aceq1  10030  aceq0  10031  aceq3lem  10033  dfac4  10035  kmlem2  10065  kmlem13  10076  axdc4lem  10368  zfac  10373  zfcndun  10528  zfcndac  10532  sup2  12099  supmul  12115  climmo  15482  summo  15642  prodmo  15861  gsumval3eu  19801  elpt  23475  gsumwrd2dccatlem  33032  1arithidomlem1  33482  1arithidom  33484  bnj1185  34759  axreg  35061  axregscl  35062  tz9.1regs  35066  fineqvac  35071  satf0op  35349  sat1el2xp  35351  cbvrexvw2  36200  cbvoprab1vw  36210  cbvoprab2vw  36211  cbvoprab13vw  36214  bj-bm1.3ii  37037  wl-ax12v2cl  37479  fdc  37724  sn-sup2  42464  cpcoll2d  44232  axc11next  44379  fnchoice  45007  ichexmpl1  47454