Metamath Proof Explorer


Theorem f1dom4g

Description: The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion f1dom4g F V A W B X F : A 1-1 B A B

Proof

Step Hyp Ref Expression
1 f1eq1 f = F f : A 1-1 B F : A 1-1 B
2 1 spcegv F V F : A 1-1 B f f : A 1-1 B
3 2 imp F V F : A 1-1 B f f : A 1-1 B
4 3 3ad2antl1 F V A W B X F : A 1-1 B f f : A 1-1 B
5 brdom2g A W B X A B f f : A 1-1 B
6 5 3adant1 F V A W B X A B f f : A 1-1 B
7 6 adantr F V A W B X F : A 1-1 B A B f f : A 1-1 B
8 4 7 mpbird F V A W B X F : A 1-1 B A B