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 ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 df-rab ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
2 1 eleq2i ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
3 id ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐵 )
4 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
6 4 5 nfan ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 )
7 sp ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) )
8 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
9 8 biimparc ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝐵 )
10 9 biantrurd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → ( 𝜑 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
11 10 bibi1d ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑥 = 𝐴 ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) )
12 11 pm5.74da ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ↔ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) ) )
13 7 12 syl5ibcom ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) → ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) ) )
14 13 imp ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) )
15 6 14 alrimi ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) )
16 elabgt ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ 𝜓 ) ) ) → ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ 𝜓 ) )
17 3 15 16 syl2an2 ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ 𝜓 ) )
18 2 17 bitrid ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝜓 ) )