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

Theorem sqxpexg 7469
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 7465 . 2 ((𝐴𝑉𝐴𝑉) → (𝐴 × 𝐴) ∈ V)
21anidms 569 1 (𝐴𝑉 → (𝐴 × 𝐴) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3493   × cxp 5546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-opab 5120  df-xp 5554  df-rel 5555
This theorem is referenced by:  resiexg  7611  erex  8305  hartogslem2  8999  harwdom  9046  dfac8b  9449  ac10ct  9452  canthwe  10065  ciclcl  17064  cicrcl  17065  cicer  17068  ssclem  17081  ipolerval  17758  mat0op  21020  matecl  21026  matlmod  21030  mattposvs  21056  ustval  22803  isust  22804  restutopopn  22839  ressuss  22864  ispsmet  22906  ismet  22925  isxmet  22926  satef  32651  satefvfmla0  32653  satefvfmla1  32660  fin2so  34866  rtrclexlem  39961  isclintop  44099  isassintop  44102  dfrngc2  44228  rngccofvalALTV  44243  dfringc2  44274  rngcresringcat  44286  ringccofvalALTV  44306
  Copyright terms: Public domain W3C validator