Metamath Proof Explorer


Theorem eqv

Description: The universe contains every set. (Contributed by NM, 11-Sep-2006) Remove dependency on ax-10 , ax-11 , ax-13 . (Revised by BJ, 10-Aug-2022)

Ref Expression
Assertion eqv A=VxxA

Proof

Step Hyp Ref Expression
1 dfcleq A=VxxAxV
2 vex xV
3 2 tbt xAxAxV
4 3 albii xxAxxAxV
5 1 4 bitr4i A=VxxA