Theorem sqxpexg 7763

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-opab 5179  df-xp 5672  df-rel 5673

This theorem is used by:  resiexg  7918  erex  8728  hartogslem2  9515  harwdom  9563  dfac8b  10034  ac10ct  10037  canthwe  10654  cicer  17888  ssclem  17901  ipolerval  18613  dfrngc2  20764  dfringc2  20793  rngcresringcat  20805  mat0op  22613  matecl  22619  matlmod  22623  mattposvs  22649  ustval  24397  isust  24398  restutopopn  24432  ressuss  24456  ispsmet  24498  ismet  24517  isxmet  24518  satef  35929  satefvfmla0  35931  satefvfmla1  35938  fin2so  38299  rtrclexlem  44383  isclintop  49013  isassintop  49016  rngccofvalALTV  49076  ringccofvalALTV  49110  2arymaptf  49473  relcic  49864