Metamath Proof Explorer

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 ⊢ X ∈ V → F ⁡ X = y z | φ
Assertion brfvopab ⊢ A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 brfvopab.1 ⊢ X ∈ V → F ⁡ X = y z | φ
2 1 breqd ⊢ X ∈ V → A F ⁡ X B ↔ A y z | φ B
3 brabv ⊢ A y z | φ B → A ∈ V ∧ B ∈ V
4 2 3 biimtrdi ⊢ X ∈ V → A F ⁡ X B → A ∈ V ∧ B ∈ V
5 4 imdistani ⊢ X ∈ V ∧ A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V
6 3anass ⊢ X ∈ V ∧ A ∈ V ∧ B ∈ V ↔ X ∈ V ∧ A ∈ V ∧ B ∈ V
7 5 6 sylibr ⊢ X ∈ V ∧ A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V
8 7 ex ⊢ X ∈ V → A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V
9 fvprc ⊢ ¬ X ∈ V → F ⁡ X = ∅
10 breq ⊢ F ⁡ X = ∅ → A F ⁡ X B ↔ A ∅ B
11 br0 ⊢ ¬ A ∅ B
12 11 pm2.21i ⊢ A ∅ B → X ∈ V ∧ A ∈ V ∧ B ∈ V
13 10 12 biimtrdi ⊢ F ⁡ X = ∅ → A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V
14 9 13 syl ⊢ ¬ X ∈ V → A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V
15 8 14 pm2.61i ⊢ A F ⁡ X B → X ∈ V ∧ A ∈ V ∧ B ∈ V