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 ⊢∀xx=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∀xx=A→φ↔ψ
5 nfv ⊢ℲxA∈B
6 4 5 nfan ⊢Ⅎx∀xx=A→φ↔ψ∧A∈B
7 sp ⊢∀xx=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 ⊢∀xx=A→φ↔ψ→A∈B→x=A→x∈B∧φ↔ψ
14 13 imp ⊢∀xx=A→φ↔ψ∧A∈B→x=A→x∈B∧φ↔ψ
15 6 14 alrimi ⊢∀xx=A→φ↔ψ∧A∈B→∀xx=A→x∈B∧φ↔ψ
16 elabgt ⊢A∈B∧∀xx=A→x∈B∧φ↔ψ→A∈x|x∈B∧φ↔ψ
17 3 15 16 syl2an2 ⊢∀xx=A→φ↔ψ∧A∈B→A∈x|x∈B∧φ↔ψ
18 2 17 bitrid ⊢∀xx=A→φ↔ψ∧A∈B→A∈x∈B|φ↔ψ