Theorem cbvexv1 2373

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2430 with a disjoint variable condition, which does not require ax-13 2403. See cbvexvw 2066 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2432 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 1886	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1886	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2372	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1810	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1810	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 304	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 324	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1567  ∃wex 1808  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-11 2191  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-nf 1813

This theorem is used by:  sb8ef  2386  exsb  2390  mof  2590  euf  2603  cbveuw  2633  eqvincf  3608  rexab2  3661  euabsn  4691  eluniab  4885  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  axrep1  5238  axrep2  5240  axrep4OLD  5244  opeliunxp  5727  opeliun2xp  5728  dfdmf  5885  dfrnf  5939  elrnmpt1  5949  cbvoprab1  7499  cbvoprab2  7500  opabex3d  7960  opabex3rd  7961  opabex3  7962  zfcndrep  10605  fsum2dlem  15828  fprod2dlem  16041  2ndresdju  33005  bnj1146  35188  bnj607  35313  bnj1228  35408  fineqvrep  35535  poimirlem26  38325  sbcexf  38792  elunif  45764  stoweidlem46  46788