Theorem sqxpexg 7705

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3432   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-opab 5142  df-xp 5631  df-rel 5632

This theorem is referenced by:  resiexg  7859  erex  8665  hartogslem2  9455  harwdom  9503  dfac8b  9951  ac10ct  9954  canthwe  10572  cicer  17771  ssclem  17784  ipolerval  18496  dfrngc2  20607  dfringc2  20636  rngcresringcat  20648  mat0op  22409  matecl  22415  matlmod  22419  mattposvs  22445  ustval  24193  isust  24194  restutopopn  24228  ressuss  24252  ispsmet  24294  ismet  24313  isxmet  24314  satef  35651  satefvfmla0  35653  satefvfmla1  35660  fin2so  37981  rtrclexlem  44067  isclintop  48705  isassintop  48708  rngccofvalALTV  48768  ringccofvalALTV  48802  2arymaptf  49150  relcic  49542