Theorem elmptrab2

Description: Membership in a one-parameter class of sets, indexed by arbitrary base sets. (Contributed by Stefan O'Rear, 28-Jul-2015) (Revised by AV, 26-Mar-2021)

	Ref	Expression
Hypotheses	elmptrab2.f	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
	elmptrab2.s1	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
	elmptrab2.s2	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
	elmptrab2.ex	⊢ 𝐵 ∈ V
	elmptrab2.rc	⊢ ( 𝑌 ∈ 𝐶 → 𝑋 ∈ 𝑊 )
Assertion	elmptrab2	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elmptrab2.f	⊢ 𝐹 = ( 𝑥 ∈ V ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
2		elmptrab2.s1	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
3		elmptrab2.s2	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
4		elmptrab2.ex	⊢ 𝐵 ∈ V
5		elmptrab2.rc	⊢ ( 𝑌 ∈ 𝐶 → 𝑋 ∈ 𝑊 )
6	4	a1i	⊢ ( 𝑥 ∈ V → 𝐵 ∈ V )
7	1 2 3 6	elmptrab	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) )
8		3simpc	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) → ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) )
9	5	elexd	⊢ ( 𝑌 ∈ 𝐶 → 𝑋 ∈ V )
10	9	adantr	⊢ ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) → 𝑋 ∈ V )
11		simpl	⊢ ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) → 𝑌 ∈ 𝐶 )
12		simpr	⊢ ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) → 𝜓 )
13	10 11 12	3jca	⊢ ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) )
14	8 13	impbii	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) )
15	7 14	bitri	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) )