Theorem cbvexvw 2036

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  cbvex2vw  2040  mojust  2542  mo4  2569  eujust  2574  cbveuvw  2608  iseqsetvlem  2808  cbvrexvw  3244  cbvrexdva2OLD  3358  euind  3746  reuind  3775  cbvopab1v  5245  cbvopab2v  5247  bm1.3ii  5320  reusv2lem2  5417  relop  5875  dmcoss  5997  fv3  6938  exfo  7139  cbvoprab3v  7542  zfun  7771  suppimacnv  8215  frrlem1  8327  wfrlem1OLD  8364  ac6sfi  9348  brwdom2  9642  ttrclss  9789  ttrclselem2  9795  aceq1  10186  aceq0  10187  aceq3lem  10189  dfac4  10191  kmlem2  10221  kmlem13  10232  axdc4lem  10524  zfac  10529  zfcndun  10684  zfcndac  10688  sup2  12251  supmul  12267  climmo  15603  summo  15765  prodmo  15984  gsumval3eu  19946  elpt  23601  1arithidomlem1  33528  1arithidom  33530  bnj1185  34769  fineqvac  35073  satf0op  35345  sat1el2xp  35347  cbvrexvw2  36193  cbvoprab1vw  36203  cbvoprab2vw  36204  cbvoprab13vw  36207  bj-bm1.3ii  37030  fdc  37705  sn-sup2  42447  cpcoll2d  44228  axc11next  44375  fnchoice  44929  ichexmpl1  47343