Theorem cnvexg 6753

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 5226	. . 3 |- Rel `' A
2		relssdmrn 5375	. . 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 4864	. . . 4 |- ran A = dom `' A
5		rnexg 6739	. . . 4 |- ( A e. V -> ran A e. _V )
6	4, 5	syl5eqelr 2512	. . 3 |- ( A e. V -> dom `' A e. _V )
7		dfdm4 5046	. . . 4 |- dom A = ran `' A
8		dmexg 6738	. . . 4 |- ( A e. V -> dom A e. _V )
9	7, 8	syl5eqelr 2512	. . 3 |- ( A e. V -> ran `' A e. _V )
10		xpexg 6607	. . 3 |- ( ( dom `' A e. _V /\ ran `' A e. _V ) -> ( dom `' A X. ran `' A ) e. _V )
11	6, 9, 10	syl2anc 665	. 2 |- ( A e. V -> ( dom `' A X. ran `' A ) e. _V )
12		ssexg 4570	. 2 |- ( ( `' A C_ ( dom `' A X. ran `' A ) /\ ( dom `' A X. ran `' A ) e. _V ) -> `' A e. _V )
13	3, 11, 12	sylancr 667	1 |- ( A e. V -> `' A e. _V )

Syntax hints:   -> wi 4   e. wcel 1872   _Vcvv 3080   C_ wss 3436   X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854   Rel wrel 4858

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-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597

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 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864

This theorem is referenced by:  cnvex  6754  relcnvexb  6755  cofunex2g  6772  tposexg  6998  cnven  7655  fopwdom  7689  domssex2  7741  domssex  7742  cnvfi  7865  mapfienlem2  7928  wemapwe  8210  fin1a2lem7  8843  fpwwe  9078  hasheqf1oi  12540  brtrclfvcnv  13068  brcnvtrclfvcnv  13069  relexpcnv  13098  relexpnnrn  13108  relexpaddg  13116  imasle  15423  cnvps  16457  gsumvalx  16512  symginv  17042  tposmap  19480  metustel  21563  metustss  21564  metustfbas  21570  metuel2  21578  psmetutop  21580  restmetu  21583  itg2gt0  22716  nlfnval  27532  cnvct  28305  ffsrn  28320  eulerpartlemgs2  29221  orvcval  29298  coinfliprv  29323  lkrval  32623  pw2f1o2val  35864  lmhmlnmsplit  35915  cnvcnvintabd  36176  clrellem  36199  relexpaddss  36280  cnvtrclfv  36286  rntrclfvRP  36293  xpexb  36777  sge0f1o  38132