Theorem prss 4184

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Hypotheses

Ref	Expression
prss.1
prss.2

Assertion

Ref	Expression
prss

Proof of Theorem prss

Step	Hyp	Ref	Expression
1		unss 3677	. 2
2		prss.1	. . . 4
3	2	snss 4154	. . 3
4		prss.2	. . . 4
5	4	snss 4154	. . 3
6	3, 5	anbi12i 697	. 2
7		df-pr 4032	. . 3
8	7	sseq1i 3527	. 2
9	1, 6, 8	3bitr4i 277	1

Syntax hints:  <->wb 184  /\wa 369  e.wcel 1818  cvv 3109  u.cun 3473  C_wss 3475  {csn 4029  {cpr 4031

This theorem is referenced by:  tpss  4195  prsspwOLD  4203  uniintsn  4324  pwssun  4791  xpsspwOLD  5122  dffv2  5946  fiint  7817  wunex2  9137  hashfun  12495  prdsle  14859  prdsless  14860  prdsleval  14874  pwsle  14889  acsfn2  15060  joinfval  15631  joindmss  15637  meetfval  15645  meetdmss  15651  clatl  15746  ipoval  15784  ipolerval  15786  eqgfval  16249  eqgval  16250  gaorb  16345  pmtrrn2  16485  efgcpbllema  16772  frgpuplem  16790  drngnidl  17877  drnglpir  17901  isnzr2hash  17912  ltbval  18136  ltbwe  18137  opsrle  18140  opsrtoslem1  18148  thlle  18728  isphtpc  21494  axlowdimlem4  24248  usgrarnedg  24384  cusgrarn  24459  frgraun  24996  frisusgranb  24997  frgra2v  24999  frgra3vlem1  25000  frgra3vlem2  25001  2pthfrgrarn  25009  frgrancvvdeqlem3  25032  shincli  26280  chincli  26378  coinfliprv  28421  altxpsspw  29627  fourierdlem103  31992  fourierdlem104  31993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-sn 4030  df-pr 4032