Theorem sqxpexg 7742

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

Step	Hyp	Ref	Expression
1		xpexg 7737	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝐴 × 𝐴) ∈ V)
2	1	anidms 576	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-opab 5167  df-xp 5657  df-rel 5658

This theorem is referenced by:  resiexg  7897  erex  8707  hartogslem2  9493  harwdom  9541  dfac8b  10003  ac10ct  10006  canthwe  10624  cicer  17851  ssclem  17864  ipolerval  18576  dfrngc2  20701  dfringc2  20730  rngcresringcat  20742  mat0op  22533  matecl  22539  matlmod  22543  mattposvs  22569  ustval  24317  isust  24318  restutopopn  24352  ressuss  24376  ispsmet  24418  ismet  24437  isxmet  24438  satef  35774  satefvfmla0  35776  satefvfmla1  35783  fin2so  38113  rtrclexlem  44199  isclintop  48828  isassintop  48831  rngccofvalALTV  48891  ringccofvalALTV  48925  2arymaptf  49284  relcic  49675