Theorem cnvexg 7903

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	⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Proof of Theorem cnvexg

Step	Hyp	Ref	Expression
1		relcnv 6078	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6244	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5652	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7881	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2834	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5862	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7880	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2834	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7730	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5281	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917   × cxp 5639  ^◡ccnv 5640  dom cdm 5641  ran crn 5642  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  cnvex  7904  relcnvexb  7905  cofunex2g  7931  tposexg  8222  cnven  9007  cnvct  9008  fopwdom  9054  domssex2  9107  domssex  9108  cnvfiALT  9297  mapfienlem2  9364  wemapwe  9657  hasheqf1oi  14323  brtrclfvcnv  14977  brcnvtrclfvcnv  14978  relexpcnv  15008  relexpnnrn  15018  relexpaddg  15026  imasle  17493  cnvps  18544  gsumvalx  18610  symginv  19339  tposmap  22351  metustel  24445  metustss  24446  metustfbas  24452  metuel2  24460  psmetutop  24462  restmetu  24465  itg2gt0  25668  nlfnval  31817  fnpreimac  32602  ffsrn  32659  pwrssmgc  32933  tocycfv  33073  elrspunidl  33406  ply1degltdimlem  33625  algextdeglem8  33721  rhmpreimacnlem  33881  eulerpartlemgs2  34378  orvcval  34456  coinfliprv  34481  cossex  38417  cosscnvex  38418  cnvelrels  38493  lkrval  39088  aks6d1c2lem4  42122  aks6d1c6lem2  42166  aks6d1c6lem3  42167  pw2f1o2val  43035  lmhmlnmsplit  43083  cnvcnvintabd  43596  clrellem  43618  relexpaddss  43714  cnvtrclfv  43720  rntrclfvRP  43727  xpexb  44450  sge0f1o  46387  smfco  46807  preimafvelsetpreimafv  47393  fundcmpsurinjlem2  47404  grimcnv  47892  grlicsym  48009  imasubclem1  49097