Theorem sqxpexg 7605

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 7600	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → (𝐴 × 𝐴) ∈ V)
2	1	anidms 567	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3432   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  resiexg  7761  erex  8522  hartogslem2  9302  harwdom  9350  dfac8b  9787  ac10ct  9790  canthwe  10407  cicer  17518  ssclem  17531  ipolerval  18250  mat0op  21568  matecl  21574  matlmod  21578  mattposvs  21604  ustval  23354  isust  23355  restutopopn  23390  ressuss  23414  ispsmet  23457  ismet  23476  isxmet  23477  satef  33378  satefvfmla0  33380  satefvfmla1  33387  fin2so  35764  rtrclexlem  41224  isclintop  45401  isassintop  45404  dfrngc2  45530  rngccofvalALTV  45545  dfringc2  45576  rngcresringcat  45588  ringccofvalALTV  45608  2arymaptf  45998