Theorem cnvexg 7863

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 6060	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6224	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5632	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7841	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2838	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5841	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7840	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2838	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7693	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5265	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898   × cxp 5619  ^◡ccnv 5620  dom cdm 5621  ran crn 5622  Rel wrel 5626

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-xp 5627  df-rel 5628  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  cnvex  7864  relcnvexb  7865  cofunex2g  7891  tposexg  8179  cnven  8966  cnvct  8967  fopwdom  9009  domssex2  9061  domssex  9062  cnvfiALT  9234  mapfienlem2  9301  wemapwe  9598  hasheqf1oi  14265  brtrclfvcnv  14918  brcnvtrclfvcnv  14919  relexpcnv  14949  relexpnnrn  14959  relexpaddg  14967  imasle  17435  cnvps  18492  gsumvalx  18592  symginv  19322  tposmap  22392  metustel  24485  metustss  24486  metustfbas  24492  metuel2  24500  psmetutop  24502  restmetu  24505  itg2gt0  25708  nlfnval  31882  fnpreimac  32675  ffsrn  32735  pwrssmgc  33010  tocycfv  33119  elrspunidl  33437  ply1degltdimlem  33707  algextdeglem8  33809  rhmpreimacnlem  33969  eulerpartlemgs2  34465  orvcval  34543  coinfliprv  34568  cossex  38594  cosscnvex  38595  cnvelrels  38661  lkrval  39260  aks6d1c2lem4  42293  aks6d1c6lem2  42337  aks6d1c6lem3  42338  pw2f1o2val  43196  lmhmlnmsplit  43244  cnvcnvintabd  43757  clrellem  43779  relexpaddss  43875  cnvtrclfv  43881  rntrclfvRP  43888  xpexb  44610  sge0f1o  46542  smfco  46962  preimafvelsetpreimafv  47550  fundcmpsurinjlem2  47561  grimcnv  48050  grlicsym  48175  imasubclem1  49265