Theorem gencbvex 1372

Description: Change of bound variable using implicit substitution.

Hypotheses

Ref	Expression
gencbvex.1	⊢ A ∈ V
gencbvex.2	⊢ (A = y → (φ ↔ ψ))
gencbvex.3	⊢ (A = y → (χ ↔ θ))
gencbvex.4	⊢ (θ ↔ ∃x(χ ∧ A = y))

Assertion

Ref	Expression
gencbvex	⊢ (∃x(χ ∧ φ) ↔ ∃y(θ ∧ ψ))

Distinct variable group(s):   ψ,x   φ,y   θ,x   χ,y   y,A

Proof of Theorem gencbvex

Step	Hyp	Ref	Expression
1		excom 728	. 2 ⊢ (∃x∃y(y = A ∧ (θ ∧ ψ)) ↔ ∃y∃x(y = A ∧ (θ ∧ ψ)))
2		gencbvex.1	. . . 4 ⊢ A ∈ V
3		gencbvex.3	. . . . . . 7 ⊢ (A = y → (χ ↔ θ))
4		gencbvex.2	. . . . . . 7 ⊢ (A = y → (φ ↔ ψ))
5	3, 4	anbi12d 476	. . . . . 6 ⊢ (A = y → ((χ ∧ φ) ↔ (θ ∧ ψ)))
6	5	bicomd 399	. . . . 5 ⊢ (A = y → ((θ ∧ ψ) ↔ (χ ∧ φ)))
7	6	cleqcoms 1104	. . . 4 ⊢ (y = A → ((θ ∧ ψ) ↔ (χ ∧ φ)))
8	2, 7	ceqsexv 1371	. . 3 ⊢ (∃y(y = A ∧ (θ ∧ ψ)) ↔ (χ ∧ φ))
9	8	biex 733	. 2 ⊢ (∃x∃y(y = A ∧ (θ ∧ ψ)) ↔ ∃x(χ ∧ φ))
10		anass 336	. . . 4 ⊢ (((∃x y = A ∧ θ) ∧ ψ) ↔ (∃x y = A ∧ (θ ∧ ψ)))
11		gencbvex.4	. . . . . 6 ⊢ (θ ↔ ∃x(χ ∧ A = y))
12	3	pm5.32i 489	. . . . . . . 8 ⊢ ((A = y ∧ χ) ↔ (A = y ∧ θ))
13		ancom 333	. . . . . . . 8 ⊢ ((A = y ∧ χ) ↔ (χ ∧ A = y))
14		cleqcom 1103	. . . . . . . . 9 ⊢ (A = y ↔ y = A)
15	14	anbi1i 368	. . . . . . . 8 ⊢ ((A = y ∧ θ) ↔ (y = A ∧ θ))
16	12, 13, 15	3bitr3 156	. . . . . . 7 ⊢ ((χ ∧ A = y) ↔ (y = A ∧ θ))
17	16	biex 733	. . . . . 6 ⊢ (∃x(χ ∧ A = y) ↔ ∃x(y = A ∧ θ))
18		19.41v 963	. . . . . 6 ⊢ (∃x(y = A ∧ θ) ↔ (∃x y = A ∧ θ))
19	11, 17, 18	3bitr 155	. . . . 5 ⊢ (θ ↔ (∃x y = A ∧ θ))
20	19	anbi1i 368	. . . 4 ⊢ ((θ ∧ ψ) ↔ ((∃x y = A ∧ θ) ∧ ψ))
21		19.41v 963	. . . 4 ⊢ (∃x(y = A ∧ (θ ∧ ψ)) ↔ (∃x y = A ∧ (θ ∧ ψ)))
22	10, 20, 21	3bitr4r 159	. . 3 ⊢ (∃x(y = A ∧ (θ ∧ ψ)) ↔ (θ ∧ ψ))
23	22	biex 733	. 2 ⊢ (∃y∃x(yx/FONT> = A ∧ (θ ∧ ψ)) ↔ ∃y(θ ∧ ψ))
24	1, 9, 23	3bitr3 156	1 ⊢ (∃x(χ ∧ φ) ↔ ∃y(θ ∧ ψ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348

This theorem is referenced by:  gencbval 1373  suppsr 4016  supsrlem6 4024  supre 4054

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org