Theorem cbvexvw 2036

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 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  2538  mo4  2565  eujust  2570  cbveuvw  2604  iseqsetvlem  2798  cbvrexvw  3221  cbvrexdva2OLD  3329  euind  3707  reuind  3736  cbvopab1v  5197  cbvopab2v  5199  bm1.3iiOLD  5272  reusv2lem2  5369  relop  5830  dmcoss  5954  fv3  6894  exfo  7095  cbvoprab3v  7499  zfun  7730  suppimacnv  8173  frrlem1  8285  wfrlem1OLD  8322  ac6sfi  9292  brwdom2  9587  ttrclss  9734  ttrclselem2  9740  aceq1  10131  aceq0  10132  aceq3lem  10134  dfac4  10136  kmlem2  10166  kmlem13  10177  axdc4lem  10469  zfac  10474  zfcndun  10629  zfcndac  10633  sup2  12198  supmul  12214  climmo  15573  summo  15733  prodmo  15952  gsumval3eu  19885  elpt  23510  gsumwrd2dccatlem  33060  1arithidomlem1  33550  1arithidom  33552  bnj1185  34824  fineqvac  35128  satf0op  35399  sat1el2xp  35401  cbvrexvw2  36245  cbvoprab1vw  36255  cbvoprab2vw  36256  cbvoprab13vw  36259  bj-bm1.3ii  37082  wl-ax12v2cl  37524  fdc  37769  sn-sup2  42514  cpcoll2d  44283  axc11next  44430  fnchoice  45053  ichexmpl1  47483