Theorem cbvexv1 2341

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-11 2159  ax-12 2179

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  sb8ef  2354  exsb  2358  mof  2557  euf  2570  cbveuw  2600  eqvincf  3603  rexab2  3656  euabsn  4677  eluniab  4871  cbvopab1  5163  cbvopab1g  5164  cbvopab2  5165  cbvopab1s  5166  axrep1  5216  axrep2  5218  axrep4OLD  5222  opeliunxp  5681  opeliun2xp  5682  dfdmf  5834  dfrnf  5887  elrnmpt1  5897  cbvoprab1  7428  cbvoprab2  7429  opabex3d  7892  opabex3rd  7893  opabex3  7894  zfcndrep  10497  fsum2dlem  15669  fprod2dlem  15879  2ndresdju  32621  bnj1146  34793  bnj607  34918  bnj1228  35013  fineqvrep  35105  poimirlem26  37665  sbcexf  38134  elunif  45032  stoweidlem46  46063