This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrab3t

Description: Membership in a restricted class abstraction, using implicit substitution. (Closed theorem version of elrab3 .) (Contributed by Thierry Arnoux, 31-Aug-2017)

Ref Expression
Assertion elrab3t ⊢ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → A ∈ x ∈ B | φ ↔ ψ

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
2 1 eleq2i ⊢ A ∈ x ∈ B | φ ↔ A ∈ x | x ∈ B ∧ φ
3 id ⊢ A ∈ B → A ∈ B
4 nfa1 ⊢ Ⅎ x ∀ x x = A → φ ↔ ψ
5 nfv ⊢ Ⅎ x A ∈ B
6 4 5 nfan ⊢ Ⅎ x ∀ x x = A → φ ↔ ψ ∧ A ∈ B
7 sp ⊢ ∀ x x = A → φ ↔ ψ → x = A → φ ↔ ψ
8 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
9 8 biimparc ⊢ A ∈ B ∧ x = A → x ∈ B
10 9 biantrurd ⊢ A ∈ B ∧ x = A → φ ↔ x ∈ B ∧ φ
11 10 bibi1d ⊢ A ∈ B ∧ x = A → φ ↔ ψ ↔ x ∈ B ∧ φ ↔ ψ
12 11 pm5.74da ⊢ A ∈ B → x = A → φ ↔ ψ ↔ x = A → x ∈ B ∧ φ ↔ ψ
13 7 12 syl5ibcom ⊢ ∀ x x = A → φ ↔ ψ → A ∈ B → x = A → x ∈ B ∧ φ ↔ ψ
14 13 imp ⊢ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → x = A → x ∈ B ∧ φ ↔ ψ
15 6 14 alrimi ⊢ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → ∀ x x = A → x ∈ B ∧ φ ↔ ψ
16 elabgt ⊢ A ∈ B ∧ ∀ x x = A → x ∈ B ∧ φ ↔ ψ → A ∈ x | x ∈ B ∧ φ ↔ ψ
17 3 15 16 syl2an2 ⊢ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → A ∈ x | x ∈ B ∧ φ ↔ ψ
18 2 17 bitrid ⊢ ∀ x x = A → φ ↔ ψ ∧ A ∈ B → A ∈ x ∈ B | φ ↔ ψ