Theorem cbvexv1 2336

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1779  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-11 2152  ax-12 2169

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-nf 1784

This theorem is referenced by:  sb8ef  2349  exsb  2353  mof  2555  euf  2568  cbveuw  2599  clelabOLD  2878  eqvincf  3637  rexab2  3694  euabsn  4729  eluniab  4922  cbvopab1  5222  cbvopab1g  5223  cbvopab2  5224  cbvopab1s  5225  axrep1  5285  axrep2  5287  axrep4  5289  opeliunxp  5742  dfdmf  5895  dfrnf  5948  elrnmpt1  5956  cbvoprab1  7498  cbvoprab2  7499  opabex3d  7954  opabex3rd  7955  opabex3  7956  zfcndrep  10611  fsum2dlem  15720  fprod2dlem  15928  2ndresdju  32141  bnj1146  34100  bnj607  34225  bnj1228  34320  fineqvrep  34393  poimirlem26  36817  sbcexf  37286  elunif  44002  stoweidlem46  45060  opeliun2xp  47096