MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnxpid Structured version   Unicode version

Theorem rnxpid 5227
Description: The range of a square Cartesian product. (Contributed by FL, 17-May-2010.)
Assertion
Ref Expression
rnxpid  |-  ran  ( A  X.  A )  =  A

Proof of Theorem rnxpid
StepHypRef Expression
1 rn0 5043 . . 3  |-  ran  (/)  =  (/)
2 xpeq2 4806 . . . . 5  |-  ( A  =  (/)  ->  ( A  X.  A )  =  ( A  X.  (/) ) )
3 xp0 5212 . . . . 5  |-  ( A  X.  (/) )  =  (/)
42, 3syl6eq 2473 . . . 4  |-  ( A  =  (/)  ->  ( A  X.  A )  =  (/) )
54rneqd 5019 . . 3  |-  ( A  =  (/)  ->  ran  ( A  X.  A )  =  ran  (/) )
6 id 22 . . 3  |-  ( A  =  (/)  ->  A  =  (/) )
71, 5, 63eqtr4a 2483 . 2  |-  ( A  =  (/)  ->  ran  ( A  X.  A )  =  A )
8 rnxp 5224 . 2  |-  ( A  =/=  (/)  ->  ran  ( A  X.  A )  =  A )
97, 8pm2.61ine 2679 1  |-  ran  ( A  X.  A )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   (/)c0 3699    X. cxp 4789   ran crn 4792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pr 4598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-br 4362  df-opab 4421  df-xp 4797  df-rel 4798  df-cnv 4799  df-dm 4801  df-rn 4802
This theorem is referenced by:  sofld  5241  fpwwe2lem13  9013  ustimasn  21180  utopbas  21187  restutop  21189  ovoliunlem1  22392  metideq  28643  poimirlem3  31850  mblfinlem1  31884  rtrclex  36137
  Copyright terms: Public domain W3C validator