Theorem cnvexg 7857

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 6055	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6217	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5630	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7835	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2833	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5838	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7834	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2833	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7687	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5262	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903   × cxp 5617  ^◡ccnv 5618  dom cdm 5619  ran crn 5620  Rel wrel 5624

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  cnvex  7858  relcnvexb  7859  cofunex2g  7885  tposexg  8173  cnven  8958  cnvct  8959  fopwdom  9002  domssex2  9054  domssex  9055  cnvfiALT  9229  mapfienlem2  9296  wemapwe  9593  hasheqf1oi  14258  brtrclfvcnv  14911  brcnvtrclfvcnv  14912  relexpcnv  14942  relexpnnrn  14952  relexpaddg  14960  imasle  17427  cnvps  18484  gsumvalx  18550  symginv  19281  tposmap  22342  metustel  24436  metustss  24437  metustfbas  24443  metuel2  24451  psmetutop  24453  restmetu  24456  itg2gt0  25659  nlfnval  31825  fnpreimac  32615  ffsrn  32673  pwrssmgc  32943  tocycfv  33052  elrspunidl  33366  ply1degltdimlem  33595  algextdeglem8  33697  rhmpreimacnlem  33857  eulerpartlemgs2  34354  orvcval  34432  coinfliprv  34457  cossex  38406  cosscnvex  38407  cnvelrels  38482  lkrval  39077  aks6d1c2lem4  42110  aks6d1c6lem2  42154  aks6d1c6lem3  42155  pw2f1o2val  43022  lmhmlnmsplit  43070  cnvcnvintabd  43583  clrellem  43605  relexpaddss  43701  cnvtrclfv  43707  rntrclfvRP  43714  xpexb  44437  sge0f1o  46373  smfco  46793  preimafvelsetpreimafv  47382  fundcmpsurinjlem2  47393  grimcnv  47882  grlicsym  48007  imasubclem1  49099