Theorem brfvopab

Description: The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021)

	Ref	Expression
Hypothesis	brfvopab.1	⊢ ( 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )
Assertion	brfvopab	⊢ ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		brfvopab.1	⊢ ( 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )
2	1	breqd	⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ↔ 𝐴 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } 𝐵 ) )
3		brabv	⊢ ( 𝐴 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4	2 3	biimtrdi	⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
5	4	imdistani	⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ) → ( 𝑋 ∈ V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
6		3anass	⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝑋 ∈ V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
7	5 6	sylibr	⊢ ( ( 𝑋 ∈ V ∧ 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ) → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
8	7	ex	⊢ ( 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
9		fvprc	⊢ ( ¬ 𝑋 ∈ V → ( 𝐹 ‘ 𝑋 ) = ∅ )
10		breq	⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 ↔ 𝐴 ∅ 𝐵 ) )
11		br0	⊢ ¬ 𝐴 ∅ 𝐵
12	11	pm2.21i	⊢ ( 𝐴 ∅ 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
13	10 12	biimtrdi	⊢ ( ( 𝐹 ‘ 𝑋 ) = ∅ → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
14	9 13	syl	⊢ ( ¬ 𝑋 ∈ V → ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
15	8 14	pm2.61i	⊢ ( 𝐴 ( 𝐹 ‘ 𝑋 ) 𝐵 → ( 𝑋 ∈ V ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) )