MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqxpexg Structured version   Visualization version   GIF version

Theorem sqxpexg 7466
Description: The Cartesian square of a set is a set. (Contributed by AV, 13-Jan-2020.)
Assertion
Ref Expression
sqxpexg (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)

Proof of Theorem sqxpexg
StepHypRef Expression
1 xpexg 7462 . 2 ((𝐴𝑉𝐴𝑉) → (𝐴 × 𝐴) ∈ V)
21anidms 567 1 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Vcvv 3492   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  resiexg  7608  erex  8302  hartogslem2  8995  harwdom  9042  dfac8b  9445  ac10ct  9448  canthwe  10061  ciclcl  17060  cicrcl  17061  cicer  17064  ssclem  17077  ipolerval  17754  mat0op  20956  matecl  20962  matlmod  20966  mattposvs  20992  ustval  22738  isust  22739  restutopopn  22774  ressuss  22799  ispsmet  22841  ismet  22860  isxmet  22861  satef  32560  satefvfmla0  32562  satefvfmla1  32569  fin2so  34760  rtrclexlem  39854  isclintop  44042  isassintop  44045  dfrngc2  44171  rngccofvalALTV  44186  dfringc2  44217  rngcresringcat  44229  ringccofvalALTV  44249
  Copyright terms: Public domain W3C validator