Theorem cbvexv1 2367

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex 2424 with a disjoint variable condition, which does not require ax-13 2397. See cbvexvw 2051 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2426 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 1871	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
3		cbvalv1.nf2	. . . . 5 ⊢ Ⅎ𝑥𝜓
4	3	nfn 1871	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
5		cbvalv1.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	5	notbid 320	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
7	2, 4, 6	cbvalv1 2366	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
8		alnex 1795	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
9		alnex 1795	. . 3 ⊢ (∀𝑦 ¬ 𝜓 ↔ ¬ ∃𝑦𝜓)
10	7, 8, 9	3bitr3i 303	. 2 ⊢ (¬ ∃𝑥𝜑 ↔ ¬ ∃𝑦𝜓)
11	10	con4bii 323	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1552  ∃wex 1793  Ⅎwnf 1797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-11 2185  ax-12 2206

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1794  df-nf 1798

This theorem is referenced by:  sb8ef  2380  exsb  2384  mof  2584  euf  2597  cbveuw  2627  eqvincf  3604  rexab2  3656  euabsn  4679  eluniab  4873  cbvopab1  5168  cbvopab1g  5169  cbvopab2  5170  cbvopab1s  5171  axrep1  5222  axrep2  5224  axrep4OLD  5228  opeliunxp  5707  opeliun2xp  5708  dfdmf  5865  dfrnf  5919  elrnmpt1  5929  cbvoprab1  7472  cbvoprab2  7473  opabex3d  7935  opabex3rd  7936  opabex3  7937  zfcndrep  10562  fsum2dlem  15773  fprod2dlem  15986  2ndresdju  32794  bnj1146  35043  bnj607  35168  bnj1228  35263  fineqvrep  35365  poimirlem26  38093  sbcexf  38562  elunif  45544  stoweidlem46  46568