Theorem sqxpexg 7731

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   × cxp 5636

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  resiexg  7888  erex  8695  hartogslem2  9496  harwdom  9544  dfac8b  9984  ac10ct  9987  canthwe  10604  cicer  17768  ssclem  17781  ipolerval  18491  dfrngc2  20537  dfringc2  20566  rngcresringcat  20578  mat0op  22306  matecl  22312  matlmod  22316  mattposvs  22342  ustval  24090  isust  24091  restutopopn  24126  ressuss  24150  ispsmet  24192  ismet  24211  isxmet  24212  satef  35403  satefvfmla0  35405  satefvfmla1  35412  fin2so  37601  rtrclexlem  43605  isclintop  48195  isassintop  48198  rngccofvalALTV  48258  ringccofvalALTV  48292  2arymaptf  48641  relcic  49034