Theorem cbvexv1 2344

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2404 with a disjoint variable condition, which does not require ax-13 2377. See cbvexvw 2036 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2406 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
cbvalv1.nf1	⊢ Ⅎ𝑦𝜑
cbvalv1.nf2	⊢ Ⅎ𝑥𝜓
cbvalv1.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvexv1	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvexv1

Step	Hyp	Ref	Expression
1		cbvalv1.nf1	. . . . 5 ⊢ Ⅎ𝑦𝜑
2	1	nfn 1857	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1857	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2343	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1781	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1781	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 321	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

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

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  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784

This theorem is referenced by:  sb8ef  2358  exsb  2362  mof  2563  euf  2576  cbveuw  2606  eqvincf  3650  rexab2  3705  euabsn  4726  eluniab  4921  cbvopab1  5217  cbvopab1g  5218  cbvopab2  5219  cbvopab1s  5220  axrep1  5280  axrep2  5282  axrep4OLD  5286  opeliunxp  5752  opeliun2xp  5753  dfdmf  5907  dfrnf  5961  elrnmpt1  5971  cbvoprab1  7520  cbvoprab2  7521  opabex3d  7990  opabex3rd  7991  opabex3  7992  zfcndrep  10654  fsum2dlem  15806  fprod2dlem  16016  2ndresdju  32659  bnj1146  34805  bnj607  34930  bnj1228  35025  fineqvrep  35109  poimirlem26  37653  sbcexf  38122  elunif  45021  stoweidlem46  46061