Theorem sqxpexg 7688

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-opab 5154  df-xp 5622  df-rel 5623

This theorem is referenced by:  resiexg  7842  erex  8646  hartogslem2  9429  harwdom  9477  dfac8b  9922  ac10ct  9925  canthwe  10542  cicer  17713  ssclem  17726  ipolerval  18438  dfrngc2  20544  dfringc2  20573  rngcresringcat  20585  mat0op  22335  matecl  22341  matlmod  22345  mattposvs  22371  ustval  24119  isust  24120  restutopopn  24154  ressuss  24178  ispsmet  24220  ismet  24239  isxmet  24240  satef  35458  satefvfmla0  35460  satefvfmla1  35467  fin2so  37653  rtrclexlem  43655  isclintop  48244  isassintop  48247  rngccofvalALTV  48307  ringccofvalALTV  48341  2arymaptf  48690  relcic  49083