Theorem elrabf

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003)

	Ref	Expression
Hypotheses	elrabf.1	⊢ Ⅎ 𝑥 𝐴
	elrabf.2	⊢ Ⅎ 𝑥 𝐵
	elrabf.3	⊢ Ⅎ 𝑥 𝜓
	elrabf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	elrabf	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elrabf.1	⊢ Ⅎ 𝑥 𝐴
2		elrabf.2	⊢ Ⅎ 𝑥 𝐵
3		elrabf.3	⊢ Ⅎ 𝑥 𝜓
4		elrabf.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5		elex	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } → 𝐴 ∈ V )
6		elex	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
7	6	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → 𝐴 ∈ V )
8		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
9	8	eleq2i	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
10	1 2	nfel	⊢ Ⅎ 𝑥 𝐴 ∈ 𝐵
11	10 3	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐵 ∧ 𝜓 )
12		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
13	12 4	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
14	1 11 13	elabgf	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
15	9 14	bitrid	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) )
16	5 7 15	pm5.21nii	⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) )