Theorem 2gencl 1366

Description: Implicit substitution for class with embedded variable.

Hypotheses

Ref	Expression
2gencl.1	⊢ (C ∈ S ↔ ∃x(x ∈ R ∧ A = C))
2gencl.2	⊢ (D ∈ S ↔ ∃y(y ∈ R ∧ B = D))
2gencl.3	⊢ (A = C → (φ ↔ ψ))
2gencl.4	⊢ (B = D → (ψ ↔ χ))
2gencl.5	⊢ ((x ∈ R ∧ y ∈ R) → φ)

Assertion

Ref	Expression
2gencl	⊢ ((C ∈ S ∧ D ∈ S) → χ)

Distinct variable group(s):   x,y   x,R   ψ,x   y,C   y,S   χ,y

Proof of Theorem 2gencl

Step	Hyp	Ref	Expression
1		2gencl.2	. . . 4 ⊢ (D ∈ S ↔ ∃y(y ∈ R ∧ B = D))
2		2gencl.4	. . . . 5 ⊢ (B = D → (ψ ↔ χ))
3	2	imbi2d 464	. . . 4 ⊢ (B = D → ((C ∈ S → ψ) ↔ (C ∈ S → χ)))
4		2gencl.1	. . . . . 6 ⊢ (C ∈ S ↔ ∃x(x ∈ R ∧ A = C))
5		2gencl.3	. . . . . . 7 ⊢ (A = C → (φ ↔ ψ))
6	5	imbi2d 464	. . . . . 6 ⊢ (A = C → ((y ∈ R → φ) ↔ (y ∈ R → ψ)))
7		2gencl.5	. . . . . . 7 ⊢ ((x ∈ R ∧ y ∈ R) → φ)
8	7	exp 291	. . . . . 6 ⊢ (x ∈ R → (y ∈ R → φ))
9	4, 6, 8	gencl 1365	. . . . 5 ⊢ (C ∈ S → (y ∈ R → ψ))
10	9	com12 13	. . . 4 ⊢ (y ∈ R → (C ∈ S → ψ))
11	1, 3, 10	gencl 1365	. . 3 ⊢ (D ∈ S → (C ∈ S → χ))
12	11	com12 13	. 2 ⊢ (C ∈ S → (D ∈ S → χ))
13	12	imp 277	1 ⊢ ((C ∈ S ∧ D ∈ S) → χ)

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

This theorem is referenced by:  3gencl 1367  axaddrcl 4067  axmulrcl 4069  axmulgt0 4086

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-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org