elrabsf

Description: Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf has implicit substitution). The hypothesis specifies that x must not be a free variable in B . (Contributed by NM, 30-Sep-2003) (Proof shortened by Mario Carneiro, 13-Oct-2016)

		Ref	Expression
	Hypothesis	elrabsf.1	⊢ Ⅎ 𝑥 𝐵
	Assertion	elrabsf	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		elrabsf.1	⊢ Ⅎ 𝑥 𝐵
2		dfsbcq	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3		nfcv	⊢ Ⅎ 𝑦 𝐵
4		nfv	⊢ Ⅎ 𝑦 𝜑
5		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
6		sbceq1a	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
7	1 3 4 5 6	cbvrabw	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ [ 𝑦 / 𝑥 ] 𝜑 }
8	2 7	elrab2	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜑 ) )

Metamath Proof Explorer

Theorem elrabsf

Proof