Theorem cnvexg 7917

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 6104	. . 3 ⊢ Rel ◡𝐴
2		relssdmrn 6268	. . 3 ⊢ (Rel ◡𝐴 → ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴))
3	1, 2	ax-mp 5	. 2 ⊢ ◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴)
4		df-rn 5670	. . . 4 ⊢ ran 𝐴 = dom ◡𝐴
5		rnexg 7895	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)
6	4, 5	eqeltrrid 2874	. . 3 ⊢ (𝐴 ∈ 𝑉 → dom ◡𝐴 ∈ V)
7		dfdm4 5883	. . . 4 ⊢ dom 𝐴 = ran ◡𝐴
8		dmexg 7894	. . . 4 ⊢ (𝐴 ∈ 𝑉 → dom 𝐴 ∈ V)
9	7, 8	eqeltrrid 2874	. . 3 ⊢ (𝐴 ∈ 𝑉 → ran ◡𝐴 ∈ V)
10	6, 9	xpexd 7746	. 2 ⊢ (𝐴 ∈ 𝑉 → (dom ◡𝐴 × ran ◡𝐴) ∈ V)
11		ssexg 5291	. 2 ⊢ ((◡𝐴 ⊆ (dom ◡𝐴 × ran ◡𝐴) ∧ (dom ◡𝐴 × ran ◡𝐴) ∈ V) → ◡𝐴 ∈ V)
12	3, 10, 11	sylancr 598	1 ⊢ (𝐴 ∈ 𝑉 → ◡𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463   ⊆ wss 3913   × cxp 5657  ^◡ccnv 5658  dom cdm 5659  ran crn 5660  Rel wrel 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pow 5334  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5665  df-rel 5666  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  cnvex  7918  relcnvexb  7919  cofunex2g  7943  tposexg  8232  cnven  9026  cnvct  9027  fopwdom  9069  domssex2  9121  domssex  9122  cnvfiALT  9292  mapfienlem2  9362  wemapwe  9662  hasheqf1oi  14383  brtrclfvcnv  15037  brcnvtrclfvcnv  15038  relexpcnv  15068  relexpnnrn  15078  relexpaddg  15086  imasle  17573  cnvps  18630  gsumvalx  18730  symginv  19468  tposmap  22579  metustel  24672  metustss  24673  metustfbas  24679  metuel2  24687  psmetutop  24689  restmetu  24692  itg2gt0  25884  oldfib  28532  nlfnval  32170  fnpreimac  32952  ffsrn  33010  pwrssmgc  33257  tocycfv  33366  elrspunidl  33676  ply1degltdimlem  33953  algextdeglem8  34055  rhmpreimacnlem  34215  eulerpartlemgs2  34711  orvcval  34789  coinfliprv  34814  cossex  39043  cosscnvex  39044  cnvelrels  39110  lkrval  39747  aks6d1c2lem4  42779  aks6d1c6lem2  42823  aks6d1c6lem3  42824  pw2f1o2val  43653  lmhmlnmsplit  43701  cnvcnvintabd  44213  clrellem  44235  relexpaddss  44331  cnvtrclfv  44337  rntrclfvRP  44344  xpexb  45049  sge0f1o  46983  smfco  47403  preimafvelsetpreimafv  48021  fundcmpsurinjlem2  48032  grimcnv  48537  grlicsym  48662  imasubclem1  49762