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

Theorem cnvss 5450
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 4848 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5154 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5274 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5274 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3787 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3715   class class class wbr 4804  {copab 4864  ccnv 5265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-in 3722  df-ss 3729  df-br 4805  df-opab 4865  df-cnv 5274
This theorem is referenced by:  cnveq  5451  rnss  5509  relcnvtr  5816  funss  6068  funres11  6127  funcnvres  6128  foimacnv  6315  funcnvuni  7284  tposss  7522  vdwnnlem1  15901  structcnvcnv  16073  catcoppccl  16959  cnvps  17413  tsrdir  17439  ustneism  22228  metustsym  22561  metust  22564  pi1xfrcnv  23057  eulerpartlemmf  30746  relcnveq3  34416  elrelscnveq3  34564  cnvssb  38394  trclubgNEW  38427  clrellem  38431  clcnvlem  38432  cnvrcl0  38434  cnvtrcl0  38435  cnvtrrel  38464  relexpaddss  38512
  Copyright terms: Public domain W3C validator