Theorem cnvexg 7947

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 6125	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6290	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5700	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7925	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2844	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5909	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7924	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2844	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7770	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5329	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963   × cxp 5687  ^◡ccnv 5688  dom cdm 5689  ran crn 5690  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  cnvex  7948  relcnvexb  7949  cofunex2g  7973  tposexg  8264  cnven  9072  cnvct  9073  fopwdom  9119  domssex2  9176  domssex  9177  cnvfiALT  9377  mapfienlem2  9444  wemapwe  9735  hasheqf1oi  14387  brtrclfvcnv  15040  brcnvtrclfvcnv  15041  relexpcnv  15071  relexpnnrn  15081  relexpaddg  15089  imasle  17570  cnvps  18636  gsumvalx  18702  symginv  19435  tposmap  22479  metustel  24579  metustss  24580  metustfbas  24586  metuel2  24594  psmetutop  24596  restmetu  24599  itg2gt0  25810  nlfnval  31910  fnpreimac  32688  ffsrn  32747  pwrssmgc  32975  tocycfv  33112  elrspunidl  33436  ply1degltdimlem  33650  algextdeglem8  33730  rhmpreimacnlem  33845  eulerpartlemgs2  34362  orvcval  34439  coinfliprv  34464  cossex  38401  cosscnvex  38402  cnvelrels  38477  lkrval  39070  aks6d1c2lem4  42109  aks6d1c6lem2  42153  aks6d1c6lem3  42154  pw2f1o2val  43028  lmhmlnmsplit  43076  cnvcnvintabd  43590  clrellem  43612  relexpaddss  43708  cnvtrclfv  43714  rntrclfvRP  43721  xpexb  44450  sge0f1o  46338  smfco  46758  preimafvelsetpreimafv  47313  fundcmpsurinjlem2  47324  grimcnv  47817  grlicsym  47909