This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) )