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

Theorem cnvss 5590
 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 4971 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5287 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5412 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5412 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3901 1 (𝐴𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3828   class class class wbr 4927  {copab 4989  ◡ccnv 5403 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-in 3835  df-ss 3842  df-br 4928  df-opab 4990  df-cnv 5412 This theorem is referenced by:  cnveq  5591  rnss  5649  relcnvtr  5956  funss  6205  funres11  6262  funcnvres  6263  foimacnv  6459  funcnvuni  7449  tposss  7693  vdwnnlem1  16181  structcnvcnv  16347  catcoppccl  17220  cnvps  17674  tsrdir  17700  ustneism  22529  metustsym  22862  metust  22865  pi1xfrcnv  23358  eulerpartlemmf  31269  relcnveq3  35000  elrelscnveq3  35154  disjss  35387  cnvssb  39286  trclubgNEW  39319  clrellem  39323  clcnvlem  39324  cnvrcl0  39326  cnvtrcl0  39327  cnvtrrel  39356  relexpaddss  39404
 Copyright terms: Public domain W3C validator