Theorem sqxpexg 7734

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   × cxp 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  resiexg  7891  erex  8698  hartogslem2  9503  harwdom  9551  dfac8b  9991  ac10ct  9994  canthwe  10611  cicer  17775  ssclem  17788  ipolerval  18498  dfrngc2  20544  dfringc2  20573  rngcresringcat  20585  mat0op  22313  matecl  22319  matlmod  22323  mattposvs  22349  ustval  24097  isust  24098  restutopopn  24133  ressuss  24157  ispsmet  24199  ismet  24218  isxmet  24219  satef  35410  satefvfmla0  35412  satefvfmla1  35419  fin2so  37608  rtrclexlem  43612  isclintop  48199  isassintop  48202  rngccofvalALTV  48262  ringccofvalALTV  48296  2arymaptf  48645  relcic  49038