Theorem sqxpexg 7229

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

Syntax hints:   → wi 4   ∈ wcel 2164  Vcvv 3414   × cxp 5344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-opab 4938  df-xp 5352  df-rel 5353

This theorem is referenced by:  resiexg  7369  erex  8038  hartogslem2  8724  harwdom  8771  dfac8b  9174  ac10ct  9177  canthwe  9795  brcic  16817  ciclcl  16821  cicrcl  16822  cicer  16825  ssclem  16838  estrccofval  17128  ipolerval  17516  mat0op  20599  matecl  20605  matlmod  20609  mattposvs  20636  ustval  22383  isust  22384  restutopopn  22419  ressuss  22444  ispsmet  22486  ismet  22505  isxmet  22506  bj-diagval  33614  fin2so  33934  rtrclexlem  38759  isclintop  42704  isassintop  42707  dfrngc2  42833  rngccofvalALTV  42848  dfringc2  42879  rngcresringcat  42891  ringccofvalALTV  42911