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