Theorem cnvexg 6745

Description: The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)

Assertion

Ref	Expression
cnvexg	|- ( A e. V -> `' A e. _V )

Proof of Theorem cnvexg

Step	Hyp	Ref	Expression
1		relcnv 5384	. . 3 |- Rel `' A
2		relssdmrn 5534	. . 3 |- ( Rel `' A -> `' A C_ ( dom `' A X. ran `' A ) )
3	1, 2	ax-mp 5	. 2 |- `' A C_ ( dom `' A X. ran `' A )
4		df-rn 5019	. . . 4 |- ran A = dom `' A
5		rnexg 6731	. . . 4 |- ( A e. V -> ran A e. _V )
6	4, 5	syl5eqelr 2550	. . 3 |- ( A e. V -> dom `' A e. _V )
7		dfdm4 5205	. . . 4 |- dom A = ran `' A
8		dmexg 6730	. . . 4 |- ( A e. V -> dom A e. _V )
9	7, 8	syl5eqelr 2550	. . 3 |- ( A e. V -> ran `' A e. _V )
10		xpexg 6601	. . 3 |- ( ( dom `' A e. _V /\ ran `' A e. _V ) -> ( dom `' A X. ran `' A ) e. _V )
11	6, 9, 10	syl2anc 661	. 2 |- ( A e. V -> ( dom `' A X. ran `' A ) e. _V )
12		ssexg 4602	. 2 |- ( ( `' A C_ ( dom `' A X. ran `' A ) /\ ( dom `' A X. ran `' A ) e. _V ) -> `' A e. _V )
13	3, 11, 12	sylancr 663	1 |- ( A e. V -> `' A e. _V )

Syntax hints:   -> wi 4   e. wcel 1819   _Vcvv 3109   C_ wss 3471   X. cxp 5006   `'ccnv 5007   dom cdm 5008   ran crn 5009   Rel wrel 5013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-xp 5014  df-rel 5015  df-cnv 5016  df-dm 5018  df-rn 5019

This theorem is referenced by:  cnvex  6746  relcnvexb  6747  cofunex2g  6764  tposexg  6987  cnven  7610  fopwdom  7644  domssex2  7696  domssex  7697  cnvfi  7822  mapfienlem2  7883  cantnfclOLD  8133  cantnflem1OLD  8148  wemapwe  8156  wemapweOLD  8157  fin1a2lem7  8803  fpwwe  9041  hasheqf1oi  12427  imasle  14940  cnvps  15969  gsumvalx  16024  symginv  16554  tposmap  19086  metustelOLD  21180  metustel  21181  metustssOLD  21182  metustss  21183  metustfbasOLD  21194  metustfbas  21195  metuel2  21208  metutopOLD  21211  psmetutop  21212  restmetu  21216  itg2gt0  22293  nlfnval  26927  cnvct  27695  ffsrn  27709  eulerpartlemgs2  28516  orvcval  28593  coinfliprv  28618  relexpcnv  29253  relexprel  29254  pw2f1o2val  31164  lmhmlnmsplit  31216  xpexb  31546  lkrval  34935