Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
The mapping operation
f1osetex
Metamath Proof Explorer
Description: The set of bijections between two classes exists. (Contributed by AV , 30-Mar-2024) (Revised by AV , 8-Aug-2024) (Proof shortened by SN , 22-Aug-2024)
Ref
Expression
Assertion
f1osetex
⊢ f | f : A ⟶ 1-1 onto B ∈ V
Proof
Step
Hyp
Ref
Expression
1
fosetex
⊢ f | f : A ⟶ onto B ∈ V
2
f1ofo
⊢ f : A ⟶ 1-1 onto B → f : A ⟶ onto B
3
2
ss2abi
⊢ f | f : A ⟶ 1-1 onto B ⊆ f | f : A ⟶ onto B
4
1 3
ssexi
⊢ f | f : A ⟶ 1-1 onto B ∈ V