Theorem sqxpexg 7702

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   × cxp 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-opab 5138  df-xp 5627  df-rel 5628

This theorem is referenced by:  resiexg  7856  erex  8662  hartogslem2  9452  harwdom  9500  dfac8b  9948  ac10ct  9951  canthwe  10569  cicer  17768  ssclem  17781  ipolerval  18493  dfrngc2  20604  dfringc2  20633  rngcresringcat  20645  mat0op  22406  matecl  22412  matlmod  22416  mattposvs  22442  ustval  24190  isust  24191  restutopopn  24225  ressuss  24249  ispsmet  24291  ismet  24310  isxmet  24311  satef  35659  satefvfmla0  35661  satefvfmla1  35668  fin2so  37989  rtrclexlem  44075  isclintop  48712  isassintop  48715  rngccofvalALTV  48775  ringccofvalALTV  48809  2arymaptf  49157  relcic  49549