Theorem cnvexg 7866

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 6063	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6227	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5635	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7844	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2841	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5844	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7843	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2841	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7696	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5268	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 587	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625  Rel wrel 5629

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 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  cnvex  7867  relcnvexb  7868  cofunex2g  7894  tposexg  8182  cnven  8970  cnvct  8971  fopwdom  9013  domssex2  9065  domssex  9066  cnvfiALT  9239  mapfienlem2  9309  wemapwe  9606  hasheqf1oi  14274  brtrclfvcnv  14927  brcnvtrclfvcnv  14928  relexpcnv  14958  relexpnnrn  14968  relexpaddg  14976  imasle  17444  cnvps  18501  gsumvalx  18601  symginv  19331  tposmap  22401  metustel  24494  metustss  24495  metustfbas  24501  metuel2  24509  psmetutop  24511  restmetu  24514  itg2gt0  25717  oldfib  28373  nlfnval  31956  fnpreimac  32749  ffsrn  32807  pwrssmgc  33082  tocycfv  33191  elrspunidl  33509  ply1degltdimlem  33779  algextdeglem8  33881  rhmpreimacnlem  34041  eulerpartlemgs2  34537  orvcval  34615  coinfliprv  34640  cossex  38682  cosscnvex  38683  cnvelrels  38749  lkrval  39348  aks6d1c2lem4  42381  aks6d1c6lem2  42425  aks6d1c6lem3  42426  pw2f1o2val  43281  lmhmlnmsplit  43329  cnvcnvintabd  43841  clrellem  43863  relexpaddss  43959  cnvtrclfv  43965  rntrclfvRP  43972  xpexb  44694  sge0f1o  46626  smfco  47046  preimafvelsetpreimafv  47634  fundcmpsurinjlem2  47645  grimcnv  48134  grlicsym  48259  imasubclem1  49349