Theorem cbvexv1 2372

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1566  ∃wex 1807  Ⅎwnf 1811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-nf 1812

This theorem is referenced by:  sb8ef  2385  exsb  2389  mof  2589  euf  2602  cbveuw  2632  eqvincf  3608  rexab2  3661  euabsn  4691  eluniab  4885  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  axrep1  5238  axrep2  5240  axrep4OLD  5244  opeliunxp  5728  opeliun2xp  5729  dfdmf  5886  dfrnf  5940  elrnmpt1  5950  cbvoprab1  7497  cbvoprab2  7498  opabex3d  7961  opabex3rd  7962  opabex3  7963  zfcndrep  10598  fsum2dlem  15821  fprod2dlem  16034  2ndresdju  32960  bnj1146  35145  bnj607  35270  bnj1228  35365  fineqvrep  35493  poimirlem26  38263  sbcexf  38732  elunif  45706  stoweidlem46  46730