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

Theorem cnvss 5204
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 id 22 . . . 4 (𝐴𝐵𝐴𝐵)
21ssbrd 4620 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
32ssopab2dv 4919 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
4 df-cnv 5036 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
5 df-cnv 5036 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
63, 4, 53sstr4g 3608 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3539   class class class wbr 4577  {copab 4636  ccnv 5027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-br 4578  df-opab 4638  df-cnv 5036
This theorem is referenced by:  cnveq  5206  rnss  5262  relcnvtr  5558  funss  5808  funres11  5866  funcnvres  5867  foimacnv  6052  funcnvuni  6989  tposss  7217  vdwnnlem1  15483  structcnvcnv  15652  catcoppccl  16527  cnvps  16981  tsrdir  17007  ustneism  21779  metustsym  22111  metust  22114  pi1xfrcnv  22596  eulerpartlemmf  29570  cnvssb  36714  trclubgNEW  36747  clrellem  36751  clcnvlem  36752  cnvrcl0  36754  cnvtrcl0  36755  cnvtrrel  36784  relexpaddss  36832
  Copyright terms: Public domain W3C validator