Theorem opabbii 4517

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 2467	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 11	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4516	. 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 184   = wceq 1379   {copab 4510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-opab 4512

This theorem is referenced by:  mptv  4545  fconstmpt  5049  xpundi  5058  xpundir  5059  inxp  5141  csbcnv  5192  cnvco  5194  resopab  5326  opabresid  5333  cnvi  5416  cnvun  5417  cnvxp  5430  cnvcnv3  5462  coundi  5514  coundir  5515  mptun  5718  fvopab6  5981  fmptsng  6093  fmptsnd  6094  cbvoprab1  6364  cbvoprab12  6366  dmoprabss  6379  mpt2mptx  6388  resoprab  6393  elrnmpt2res  6411  ov6g  6435  1st2val  6821  2nd2val  6822  dfoprab3s  6850  dfoprab3  6851  dfoprab4  6852  fsplit  6900  mapsncnv  7477  xpcomco  7619  marypha2lem2  7908  oemapso  8113  leweon  8401  r0weon  8402  compsscnv  8763  fpwwe  9036  ltrelxr  9660  ltxrlt  9667  ltxr  11336  shftidt2  12893  prdsle  14733  prdsless  14734  prdsleval  14748  joindm  15506  meetdm  15520  gaorb  16216  efgcpbllema  16643  frgpuplem  16661  ltbval  18004  ltbwe  18005  opsrle  18008  opsrtoslem1  18016  opsrtoslem2  18017  dvdsrzring  18374  dvdsrz  18375  pjfval2  18607  lmfval  19599  lmbr  19625  cnmptid  20028  lgsquadlem3  23495  perpln1  23942  axcontlem2  24100  wlks  24351  trls  24370  dfconngra1  24503  dfadj2  26635  dmadjss  26637  cnvadj  26642  mpt2mptxf  27349  dfid4  28935  fneer  30105  opropabco  30148  fgraphopab  31105  fgraphxp  31106  xpsnopab  32249  mpt2mptx2  32409  cmtfvalN  34413  cmtvalN  34414  cvrfval  34471  cvrval  34472  dicval2  36382