Theorem cbvexv1 2332

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1531  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-11 2146  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778

This theorem is referenced by:  sb8ef  2345  exsb  2349  mof  2551  euf  2564  cbveuw  2594  clelabOLD  2872  eqvincf  3634  rexab2  3692  euabsn  4731  eluniab  4922  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  axrep1  5286  axrep2  5288  axrep4  5290  opeliunxp  5744  dfdmf  5898  dfrnf  5951  elrnmpt1  5959  cbvoprab1  7505  cbvoprab2  7506  opabex3d  7968  opabex3rd  7969  opabex3  7970  zfcndrep  10637  fsum2dlem  15748  fprod2dlem  15956  2ndresdju  32492  bnj1146  34492  bnj607  34617  bnj1228  34712  fineqvrep  34785  poimirlem26  37189  sbcexf  37658  elunif  44443  stoweidlem46  45497  opeliun2xp  47508