Theorem cnvexg 6727

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 5185	. . 3 |- Rel `' A
2		relssdmrn 5335	. . 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 4823	. . . 4 |- ran A = dom `' A
5		rnexg 6713	. . . 4 |- ( A e. V -> ran A e. _V )
6	4, 5	syl5eqelr 2535	. . 3 |- ( A e. V -> dom `' A e. _V )
7		dfdm4 5005	. . . 4 |- dom A = ran `' A
8		dmexg 6712	. . . 4 |- ( A e. V -> dom A e. _V )
9	7, 8	syl5eqelr 2535	. . 3 |- ( A e. V -> ran `' A e. _V )
10		xpexg 6581	. . 3 |- ( ( dom `' A e. _V /\ ran `' A e. _V ) -> ( dom `' A X. ran `' A ) e. _V )
11	6, 9, 10	syl2anc 671	. 2 |- ( A e. V -> ( dom `' A X. ran `' A ) e. _V )
12		ssexg 4521	. 2 |- ( ( `' A C_ ( dom `' A X. ran `' A ) /\ ( dom `' A X. ran `' A ) e. _V ) -> `' A e. _V )
13	3, 11, 12	sylancr 674	1 |- ( A e. V -> `' A e. _V )

Syntax hints:   -> wi 4   e. wcel 1891   _Vcvv 3013   C_ wss 3372   X. cxp 4810   `'ccnv 4811   dom cdm 4812   ran crn 4813   Rel wrel 4817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-xp 4818  df-rel 4819  df-cnv 4820  df-dm 4822  df-rn 4823

This theorem is referenced by:  cnvex  6728  relcnvexb  6729  cofunex2g  6746  tposexg  6974  cnven  7632  fopwdom  7667  domssex2  7719  domssex  7720  cnvfi  7843  mapfienlem2  7906  wemapwe  8189  fin1a2lem7  8823  fpwwe  9058  hasheqf1oi  12528  brtrclfvcnv  13079  brcnvtrclfvcnv  13080  relexpcnv  13109  relexpnnrn  13119  relexpaddg  13127  imasle  15435  cnvps  16469  gsumvalx  16524  symginv  17054  tposmap  19493  metustel  21576  metustss  21577  metustfbas  21583  metuel2  21591  psmetutop  21593  restmetu  21596  itg2gt0  22730  nlfnval  27546  cnvct  28307  ffsrn  28322  eulerpartlemgs2  29219  orvcval  29296  coinfliprv  29321  lkrval  32656  pw2f1o2val  35896  lmhmlnmsplit  35947  cnvcnvintabd  36208  clrellem  36231  relexpaddss  36312  cnvtrclfv  36318  rntrclfvRP  36325  xpexb  36808  sge0f1o  38283