Theorem cnvexg 7875

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 6069	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6233	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5642	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7853	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2841	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5850	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7852	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2841	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7705	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5264	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 588	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889   × cxp 5629  ^◡ccnv 5630  dom cdm 5631  ran crn 5632  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  cnvex  7876  relcnvexb  7877  cofunex2g  7903  tposexg  8190  cnven  8980  cnvct  8981  fopwdom  9023  domssex2  9075  domssex  9076  cnvfiALT  9249  mapfienlem2  9319  wemapwe  9618  hasheqf1oi  14313  brtrclfvcnv  14966  brcnvtrclfvcnv  14967  relexpcnv  14997  relexpnnrn  15007  relexpaddg  15015  imasle  17487  cnvps  18544  gsumvalx  18644  symginv  19377  tposmap  22422  metustel  24515  metustss  24516  metustfbas  24522  metuel2  24530  psmetutop  24532  restmetu  24535  itg2gt0  25727  oldfib  28369  nlfnval  31952  fnpreimac  32743  ffsrn  32801  pwrssmgc  33060  tocycfv  33170  elrspunidl  33488  ply1degltdimlem  33766  algextdeglem8  33868  rhmpreimacnlem  34028  eulerpartlemgs2  34524  orvcval  34602  coinfliprv  34627  cossex  38830  cosscnvex  38831  cnvelrels  38897  lkrval  39534  aks6d1c2lem4  42566  aks6d1c6lem2  42610  aks6d1c6lem3  42611  pw2f1o2val  43467  lmhmlnmsplit  43515  cnvcnvintabd  44027  clrellem  44049  relexpaddss  44145  cnvtrclfv  44151  rntrclfvRP  44158  xpexb  44880  sge0f1o  46810  smfco  47230  preimafvelsetpreimafv  47848  fundcmpsurinjlem2  47859  grimcnv  48364  grlicsym  48489  imasubclem1  49579