Theorem opabbii 4460

Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.)

Hypothesis

Ref	Expression
opabbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
opabbii	|- { <. x , y >. | ph } = { <. x , y >. | ps }

Proof of Theorem opabbii

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2471	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 11	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4459	. 2 |- ( z = z -> { <. x , y >. | ph } = { <. x , y >. | ps } )
5	1, 4	ax-mp 5	1 |- { <. x , y >. | ph } = { <. x , y >. | ps }

Syntax hints:   <-> wb 189   = wceq 1452   {copab 4453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-opab 4455

This theorem is referenced by:  mptv  4489  2rbropap  4742  dfid4  4756  fconstmpt  4883  xpundi  4892  xpundir  4893  inxp  4972  csbcnv  5023  cnvco  5025  resopab  5157  opabresid  5164  cnvi  5246  cnvun  5247  cnvxp  5260  cnvcnv3  5291  coundi  5343  coundir  5344  mptun  5719  fvopab6  5990  fmptsng  6101  fmptsnd  6102  fvmptopab2  6352  cbvoprab1  6382  cbvoprab12  6384  dmoprabss  6397  mpt2mptx  6406  resoprab  6411  elrnmpt2res  6429  ov6g  6453  1st2val  6838  2nd2val  6839  dfoprab3s  6867  dfoprab3  6868  dfoprab4  6869  fsplit  6920  mapsncnv  7536  xpcomco  7680  marypha2lem2  7968  oemapso  8205  leweon  8460  r0weon  8461  compsscnv  8819  fpwwe  9089  ltrelxr  9713  ltxrlt  9722  ltxr  11438  shftidt2  13221  prdsle  15438  prdsless  15439  prdsleval  15453  dfiso2  15755  joindm  16327  meetdm  16341  gaorb  17039  efgcpbllema  17482  frgpuplem  17500  ltbval  18772  ltbwe  18773  opsrle  18776  opsrtoslem1  18784  opsrtoslem2  18785  dvdsrzring  19129  pjfval2  19349  lmfval  20325  lmbr  20351  cnmptid  20753  lgsquadlem3  24363  perpln1  24834  outpasch  24876  ishpg  24880  axcontlem2  25074  wlks  25326  trls  25345  dfconngra1  25478  dfadj2  27619  dmadjss  27621  cnvadj  27626  mpt2mptxf  28355  fneer  31080  bj-dfmpt2a  31700  bj-mpt2mptALT  31701  opropabco  32114  cmtfvalN  32847  cmtvalN  32848  cvrfval  32905  cvrval  32906  dicval2  34818  fgraphopab  36158  fgraphxp  36159  opabn1stprc  39153  opabbrfex0d  39176  opabbrfexd  39178  mptmpt2opabbrd  39180  1wlksfval  39813  wlksfval  39814  wlkson  39854  xpsnopab  40273  mpt2mptx2  40624