This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Jonathan Ben-Naim First-order logic and set theory bnj519
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim , 3-Jun-2011) (Revised by Mario Carneiro , 6-May-2015)
(New usage is discouraged.)
Ref
Expression
Hypothesis
bnj519.1 ⊢ 𝐴 ∈ V
Assertion
bnj519 ⊢ ( 𝐵 ∈ V → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )
Proof
Step
Hyp
Ref
Expression
1
bnj519.1 ⊢ 𝐴 ∈ V
2
funsng ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )
3
1 2
mpan ⊢ ( 𝐵 ∈ V → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )