Theorem cnvexg 7849

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 6048	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6211	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5622	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7827	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2836	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5830	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7826	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2836	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7679	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5256	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897   × cxp 5609  ^◡ccnv 5610  dom cdm 5611  ran crn 5612  Rel wrel 5616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-xp 5617  df-rel 5618  df-cnv 5619  df-dm 5621  df-rn 5622

This theorem is referenced by:  cnvex  7850  relcnvexb  7851  cofunex2g  7877  tposexg  8165  cnven  8950  cnvct  8951  fopwdom  8993  domssex2  9045  domssex  9046  cnvfiALT  9218  mapfienlem2  9285  wemapwe  9582  hasheqf1oi  14253  brtrclfvcnv  14906  brcnvtrclfvcnv  14907  relexpcnv  14937  relexpnnrn  14947  relexpaddg  14955  imasle  17422  cnvps  18479  gsumvalx  18579  symginv  19309  tposmap  22367  metustel  24460  metustss  24461  metustfbas  24467  metuel2  24475  psmetutop  24477  restmetu  24480  itg2gt0  25683  nlfnval  31853  fnpreimac  32645  ffsrn  32703  pwrssmgc  32973  tocycfv  33070  elrspunidl  33385  ply1degltdimlem  33627  algextdeglem8  33729  rhmpreimacnlem  33889  eulerpartlemgs2  34385  orvcval  34463  coinfliprv  34488  cossex  38456  cosscnvex  38457  cnvelrels  38532  lkrval  39127  aks6d1c2lem4  42160  aks6d1c6lem2  42204  aks6d1c6lem3  42205  pw2f1o2val  43072  lmhmlnmsplit  43120  cnvcnvintabd  43633  clrellem  43655  relexpaddss  43751  cnvtrclfv  43757  rntrclfvRP  43764  xpexb  44486  sge0f1o  46420  smfco  46840  preimafvelsetpreimafv  47419  fundcmpsurinjlem2  47430  grimcnv  47919  grlicsym  48044  imasubclem1  49136