MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvss Structured version   Visualization version   GIF version

Theorem cnvss 5711
Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Kyle Wyonch, 27-Apr-2021.)
Assertion
Ref Expression
cnvss (𝐴𝐵𝐴𝐵)

Proof of Theorem cnvss
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssbr 5077 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5406 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5531 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5531 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3963 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3884   class class class wbr 5033  {copab 5095  ccnv 5522
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-br 5034  df-opab 5096  df-cnv 5531
This theorem is referenced by:  cnveq  5712  rnss  5777  relcnvtrg  6090  funss  6347  funres11  6405  funcnvres  6406  foimacnv  6611  funcnvuni  7622  tposss  7880  vdwnnlem1  16325  structcnvcnv  16493  catcoppccl  17364  cnvps  17818  tsrdir  17844  ustneism  22833  metustsym  23166  metust  23169  pi1xfrcnv  23666  eulerpartlemmf  31747  relcnveq3  35737  elrelscnveq3  35890  disjss  36123  cnvssb  40279  trclubgNEW  40311  clrellem  40315  clcnvlem  40316  cnvrcl0  40318  cnvtrcl0  40319  cnvtrrel  40364  relexpaddss  40412
  Copyright terms: Public domain W3C validator