Theorem opabbii 4466

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 2450	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 11	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4465	. 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 188   = wceq 1443   {copab 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-opab 4461

This theorem is referenced by:  mptv  4495  dfid4  4750  fconstmpt  4877  xpundi  4886  xpundir  4887  inxp  4966  csbcnv  5017  cnvco  5019  resopab  5150  opabresid  5157  cnvi  5239  cnvun  5240  cnvxp  5253  cnvcnv3  5284  coundi  5335  coundir  5336  mptun  5707  fvopab6  5973  fmptsng  6083  fmptsnd  6084  cbvoprab1  6360  cbvoprab12  6362  dmoprabss  6375  mpt2mptx  6384  resoprab  6389  elrnmpt2res  6407  ov6g  6431  1st2val  6816  2nd2val  6817  dfoprab3s  6845  dfoprab3  6846  dfoprab4  6847  fsplit  6898  mapsncnv  7515  xpcomco  7659  marypha2lem2  7947  oemapso  8184  leweon  8439  r0weon  8440  compsscnv  8798  fpwwe  9068  ltrelxr  9692  ltxrlt  9701  ltxr  11412  shftidt2  13137  prdsle  15353  prdsless  15354  prdsleval  15368  dfiso2  15670  joindm  16242  meetdm  16256  gaorb  16954  efgcpbllema  17397  frgpuplem  17415  ltbval  18688  ltbwe  18689  opsrle  18692  opsrtoslem1  18700  opsrtoslem2  18701  dvdsrzring  19045  pjfval2  19265  lmfval  20241  lmbr  20267  cnmptid  20669  lgsquadlem3  24277  perpln1  24748  outpasch  24790  ishpg  24794  axcontlem2  24988  wlks  25240  trls  25259  dfconngra1  25392  dfadj2  27531  dmadjss  27533  cnvadj  27538  mpt2mptxf  28273  fneer  31002  bj-dfmpt2a  31623  bj-mpt2mptALT  31624  opropabco  32043  cmtfvalN  32770  cmtvalN  32771  cvrfval  32828  cvrval  32829  dicval2  34741  fgraphopab  36081  fgraphxp  36082  opabn1stprc  39001  1wlksfval  39609  wlksfval  39610  xpsnopab  39752  mpt2mptx2  40103