Metamath Proof Explorer


Theorem rr-grothshortbi

Description: Express "every set is contained in a Grothendieck universe" in a short form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 8-Oct-2024)

Ref Expression
Assertion rr-grothshortbi xyUnivxyxyxyzyf𝒫ywy𝒫zywzff𝒫𝒫w

Proof

Step Hyp Ref Expression
1 df-rex yUnivxyyyUnivxy
2 exancom yyUnivxyyxyyUniv
3 dfuniv2 Univ=y|zyf𝒫ywy𝒫zywzff𝒫𝒫w
4 3 eqabri yUnivzyf𝒫ywy𝒫zywzff𝒫𝒫w
5 4 anbi2i xyyUnivxyzyf𝒫ywy𝒫zywzff𝒫𝒫w
6 5 exbii yxyyUnivyxyzyf𝒫ywy𝒫zywzff𝒫𝒫w
7 1 2 6 3bitri yUnivxyyxyzyf𝒫ywy𝒫zywzff𝒫𝒫w
8 7 albii xyUnivxyxyxyzyf𝒫ywy𝒫zywzff𝒫𝒫w