Theorem cbvexvw 2037

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2400 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  2533  mo4  2560  eujust  2565  cbveuvw  2599  iseqsetvlem  2793  cbvrexvw  3217  cbvrexdva2OLD  3325  euind  3698  reuind  3727  cbvopab1v  5188  cbvopab2v  5189  bm1.3iiOLD  5260  reusv2lem2  5357  relop  5817  dmcoss  5941  fv3  6879  exfo  7080  cbvoprab3v  7484  zfun  7715  suppimacnv  8156  frrlem1  8268  ac6sfi  9238  brwdom2  9533  ttrclss  9680  ttrclselem2  9686  aceq1  10077  aceq0  10078  aceq3lem  10080  dfac4  10082  kmlem2  10112  kmlem13  10123  axdc4lem  10415  zfac  10420  zfcndun  10575  zfcndac  10579  sup2  12146  supmul  12162  climmo  15530  summo  15690  prodmo  15909  gsumval3eu  19841  elpt  23466  gsumwrd2dccatlem  33013  1arithidomlem1  33513  1arithidom  33515  bnj1185  34790  fineqvac  35094  satf0op  35371  sat1el2xp  35373  cbvrexvw2  36222  cbvoprab1vw  36232  cbvoprab2vw  36233  cbvoprab13vw  36236  bj-bm1.3ii  37059  wl-ax12v2cl  37501  fdc  37746  sn-sup2  42486  cpcoll2d  44255  axc11next  44402  fnchoice  45030  ichexmpl1  47474