Theorem cbvexvw 2036

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2406 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 2035	. . 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 2007

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

This theorem is referenced by:  cbvex2vw  2040  mojust  2539  mo4  2566  eujust  2571  cbveuvw  2605  iseqsetvlem  2805  cbvrexvw  3238  cbvrexdva2OLD  3350  euind  3730  reuind  3759  cbvopab1v  5221  cbvopab2v  5223  bm1.3iiOLD  5302  reusv2lem2  5399  relop  5861  dmcoss  5985  fv3  6924  exfo  7125  cbvoprab3v  7525  zfun  7756  suppimacnv  8199  frrlem1  8311  wfrlem1OLD  8348  ac6sfi  9320  brwdom2  9613  ttrclss  9760  ttrclselem2  9766  aceq1  10157  aceq0  10158  aceq3lem  10160  dfac4  10162  kmlem2  10192  kmlem13  10203  axdc4lem  10495  zfac  10500  zfcndun  10655  zfcndac  10659  sup2  12224  supmul  12240  climmo  15593  summo  15753  prodmo  15972  gsumval3eu  19922  elpt  23580  gsumwrd2dccatlem  33069  1arithidomlem1  33563  1arithidom  33565  bnj1185  34807  fineqvac  35111  satf0op  35382  sat1el2xp  35384  cbvrexvw2  36228  cbvoprab1vw  36238  cbvoprab2vw  36239  cbvoprab13vw  36242  bj-bm1.3ii  37065  wl-ax12v2cl  37507  fdc  37752  sn-sup2  42501  cpcoll2d  44278  axc11next  44425  fnchoice  45034  ichexmpl1  47456