Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axgroth5 Unicode version

Theorem axgroth5 8655
 Description: The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)
Assertion
Ref Expression
axgroth5
Distinct variable group:   ,,,

Proof of Theorem axgroth5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax-groth 8654 . 2
2 biid 228 . . . 4
3 pwss 3773 . . . . . 6
4 pwss 3773 . . . . . . 7
54rexbii 2691 . . . . . 6
63, 5anbi12i 679 . . . . 5
76ralbii 2690 . . . 4
8 df-ral 2671 . . . . 5
9 vex 2919 . . . . . . . 8
109elpw 3765 . . . . . . 7
1110imbi1i 316 . . . . . 6
1211albii 1572 . . . . 5
138, 12bitri 241 . . . 4
142, 7, 133anbi123i 1142 . . 3
1514exbii 1589 . 2
161, 15mpbir 201 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 358   wa 359   w3a 936  wal 1546  wex 1547   wcel 1721  wral 2666  wrex 2667   wss 3280  cpw 3759   class class class wbr 4172   cen 7065 This theorem is referenced by:  grothpw  8657  grothpwex  8658  axgroth6  8659  grothtsk  8666 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-groth 8654 This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761
 Copyright terms: Public domain W3C validator