Metamath Proof Explorer


Theorem dfss3f

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004)

Ref Expression
Hypotheses dfssf.1 _ x A
dfssf.2 _ x B
Assertion dfss3f A B x A x B

Proof

Step Hyp Ref Expression
1 dfssf.1 _ x A
2 dfssf.2 _ x B
3 1 2 dfssf A B x x A x B
4 df-ral x A x B x x A x B
5 3 4 bitr4i A B x A x B