Metamath Proof Explorer

Theorem rababg

Description: Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020)

Ref Expression
Assertion rababg ⊢ ∀ x φ → x ∈ A ↔ x ∈ A | φ = x | φ

Proof

Step Hyp Ref Expression
1 ancrb ⊢ φ → x ∈ A ↔ φ → x ∈ A ∧ φ
2 1 albii ⊢ ∀ x φ → x ∈ A ↔ ∀ x φ → x ∈ A ∧ φ
3 nfv ⊢ Ⅎ y φ → x ∈ A ∧ φ
4 nfsab1 ⊢ Ⅎ x y ∈ x | φ
5 nfrab1 ⊢ Ⅎ _ x x ∈ A | φ
6 5 nfcri ⊢ Ⅎ x y ∈ x ∈ A | φ
7 4 6 nfim ⊢ Ⅎ x y ∈ x | φ → y ∈ x ∈ A | φ
8 abid ⊢ x ∈ x | φ ↔ φ
9 eleq1w ⊢ x = y → x ∈ x | φ ↔ y ∈ x | φ
10 8 9 bitr3id ⊢ x = y → φ ↔ y ∈ x | φ
11 rabid ⊢ x ∈ x ∈ A | φ ↔ x ∈ A ∧ φ
12 eleq1w ⊢ x = y → x ∈ x ∈ A | φ ↔ y ∈ x ∈ A | φ
13 11 12 bitr3id ⊢ x = y → x ∈ A ∧ φ ↔ y ∈ x ∈ A | φ
14 10 13 imbi12d ⊢ x = y → φ → x ∈ A ∧ φ ↔ y ∈ x | φ → y ∈ x ∈ A | φ
15 3 7 14 cbvalv1 ⊢ ∀ x φ → x ∈ A ∧ φ ↔ ∀ y y ∈ x | φ → y ∈ x ∈ A | φ
16 eqss ⊢ x ∈ A | φ = x | φ ↔ x ∈ A | φ ⊆ x | φ ∧ x | φ ⊆ x ∈ A | φ
17 rabssab ⊢ x ∈ A | φ ⊆ x | φ
18 17 biantrur ⊢ x | φ ⊆ x ∈ A | φ ↔ x ∈ A | φ ⊆ x | φ ∧ x | φ ⊆ x ∈ A | φ
19 df-ss ⊢ x | φ ⊆ x ∈ A | φ ↔ ∀ y y ∈ x | φ → y ∈ x ∈ A | φ
20 16 18 19 3bitr2ri ⊢ ∀ y y ∈ x | φ → y ∈ x ∈ A | φ ↔ x ∈ A | φ = x | φ
21 2 15 20 3bitri ⊢ ∀ x φ → x ∈ A ↔ x ∈ A | φ = x | φ