Theorem cnvexg 7864

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 6056	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6220	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5629	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7842	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2844	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5837	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7841	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2844	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7694	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5251	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 593	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   ⊆ wss 3883   × cxp 5616  ^◡ccnv 5617  dom cdm 5618  ran crn 5619  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  cnvex  7865  relcnvexb  7866  cofunex2g  7892  tposexg  8180  cnven  8970  cnvct  8971  fopwdom  9013  domssex2  9065  domssex  9066  cnvfiALT  9239  mapfienlem2  9309  wemapwe  9609  hasheqf1oi  14304  brtrclfvcnv  14957  brcnvtrclfvcnv  14958  relexpcnv  14988  relexpnnrn  14998  relexpaddg  15006  imasle  17478  cnvps  18535  gsumvalx  18635  symginv  19368  tposmap  22440  metustel  24533  metustss  24534  metustfbas  24540  metuel2  24548  psmetutop  24550  restmetu  24553  itg2gt0  25745  oldfib  28387  nlfnval  31970  fnpreimac  32762  ffsrn  32820  pwrssmgc  33079  tocycfv  33190  elrspunidl  33511  ply1degltdimlem  33806  algextdeglem8  33908  rhmpreimacnlem  34068  eulerpartlemgs2  34564  orvcval  34642  coinfliprv  34667  cossex  38876  cosscnvex  38877  cnvelrels  38943  lkrval  39580  aks6d1c2lem4  42612  aks6d1c6lem2  42656  aks6d1c6lem3  42657  pw2f1o2val  43484  lmhmlnmsplit  43532  cnvcnvintabd  44044  clrellem  44066  relexpaddss  44162  cnvtrclfv  44168  rntrclfvRP  44175  xpexb  44897  sge0f1o  46825  smfco  47245  preimafvelsetpreimafv  47863  fundcmpsurinjlem2  47874  grimcnv  48379  grlicsym  48504  imasubclem1  49594