Theorem cnvexg 6536

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 5218	. . 3 |- Rel `' A
2		relssdmrn 5370	. . 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 4863	. . . 4 |- ran A = dom `' A
5		rnexg 6522	. . . 4 |- ( A e. V -> ran A e. _V )
6	4, 5	syl5eqelr 2528	. . 3 |- ( A e. V -> dom `' A e. _V )
7		dfdm4 5044	. . . 4 |- dom A = ran `' A
8		dmexg 6521	. . . 4 |- ( A e. V -> dom A e. _V )
9	7, 8	syl5eqelr 2528	. . 3 |- ( A e. V -> ran `' A e. _V )
10		xpexg 6519	. . 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 4450	. 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 1756   _Vcvv 2984   C_ wss 3340   X. cxp 4850   `'ccnv 4851   dom cdm 4852   ran crn 4853   Rel wrel 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-xp 4858  df-rel 4859  df-cnv 4860  df-dm 4862  df-rn 4863

This theorem is referenced by:  cnvex  6537  relcnvexb  6538  cofunex2g  6554  tposexg  6771  cnven  7397  fopwdom  7431  domssex2  7483  domssex  7484  cnvfi  7607  mapfienlem2  7667  cantnfclOLD  7917  cantnflem1OLD  7932  wemapwe  7940  wemapweOLD  7941  fin1a2lem7  8587  fpwwe  8825  hasheqf1oi  12134  imasle  14473  cnvps  15394  gsumvalx  15514  symginv  15919  tposmap  18354  metustelOLD  20138  metustel  20139  metustssOLD  20140  metustss  20141  metustfbasOLD  20152  metustfbas  20153  metuel2  20166  metutopOLD  20169  psmetutop  20170  restmetu  20174  itg2gt0  21250  nlfnval  25297  cnvct  26027  ffsrn  26041  eulerpartlemgs2  26775  orvcval  26852  coinfliprv  26877  relexpcnv  27347  relexprel  27348  pw2f1o2val  29400  lmhmlnmsplit  29452  xpexb  29722  lkrval  32745