Theorem cbvexv1 2343

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2403 with a disjoint variable condition, which does not require ax-13 2376. See cbvexvw 2036 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2405 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 2342	. . 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 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  sb8ef  2357  exsb  2361  mof  2562  euf  2575  cbveuw  2605  eqvincf  3629  rexab2  3682  euabsn  4702  eluniab  4897  cbvopab1  5193  cbvopab1g  5194  cbvopab2  5195  cbvopab1s  5196  axrep1  5250  axrep2  5252  axrep4OLD  5256  opeliunxp  5721  opeliun2xp  5722  dfdmf  5876  dfrnf  5930  elrnmpt1  5940  cbvoprab1  7494  cbvoprab2  7495  opabex3d  7964  opabex3rd  7965  opabex3  7966  zfcndrep  10628  fsum2dlem  15786  fprod2dlem  15996  2ndresdju  32627  bnj1146  34822  bnj607  34947  bnj1228  35042  fineqvrep  35126  poimirlem26  37670  sbcexf  38139  elunif  45040  stoweidlem46  46075