Theorem sqxpexg 7709

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  resiexg  7863  erex  8668  hartogslem2  9458  harwdom  9506  dfac8b  9953  ac10ct  9956  canthwe  10574  cicer  17773  ssclem  17786  ipolerval  18498  dfrngc2  20605  dfringc2  20634  rngcresringcat  20646  mat0op  22384  matecl  22390  matlmod  22394  mattposvs  22420  ustval  24168  isust  24169  restutopopn  24203  ressuss  24227  ispsmet  24269  ismet  24288  isxmet  24289  satef  35598  satefvfmla0  35600  satefvfmla1  35607  fin2so  37928  rtrclexlem  44043  isclintop  48683  isassintop  48686  rngccofvalALTV  48746  ringccofvalALTV  48780  2arymaptf  49128  relcic  49520