Theorem sqxpexg 7758

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-opab 5168  df-xp 5657  df-rel 5658

This theorem is used by:  resiexg  7913  erex  8726  hartogslem2  9521  harwdom  9569  dfac8b  10091  ac10ct  10094  canthwe  10717  cicer  17961  ssclem  17974  ipolerval  18686  dfrngc2  20860  dfringc2  20889  rngcresringcat  20901  mat0op  22714  matecl  22720  matlmod  22724  mattposvs  22750  ustval  24502  isust  24503  restutopopn  24537  ressuss  24561  ispsmet  24603  ismet  24622  isxmet  24623  satef  36150  satefvfmla0  36152  satefvfmla1  36159  fin2so  38498  rtrclexlem  44575  isclintop  49248  isassintop  49251  rngccofvalALTV  49311  ringccofvalALTV  49345  2arymaptf  49708  relcic  50097  veronesematbasd  50924  veroquaddetzerod  50930