Theorem opabbii 4355

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 2442	. 2 |- z = z
2		opabbii.1	. . . 4 |- ( ph <-> ps )
3	2	a1i 11	. . 3 |- ( z = z -> ( ph <-> ps ) )
4	3	opabbidv 4354	. 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 1369   {copab 4348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-opab 4350

This theorem is referenced by:  mptv  4383  fconstmpt  4881  xpundi  4890  xpundir  4891  inxp  4971  csbcnv  5022  cnvco  5024  resopab  5152  opabresid  5158  cnvi  5240  cnvun  5241  cnvxp  5254  cnvcnv3  5286  coundi  5338  coundir  5339  mptun  5540  fvopab6  5795  fmptsng  5899  cbvoprab1  6157  cbvoprab12  6159  dmoprabss  6171  mpt2mptx  6180  resoprab  6185  elrnmpt2res  6203  ov6g  6227  1st2val  6601  2nd2val  6602  dfoprab3s  6628  dfoprab3  6629  dfoprab4  6630  fsplit  6676  mapsncnv  7258  xpcomco  7400  marypha2lem2  7685  oemapso  7889  leweon  8177  r0weon  8178  compsscnv  8539  fpwwe  8812  ltrelxr  9437  ltxrlt  9444  ltxr  11094  shftidt2  12569  prdsle  14399  prdsless  14400  prdsleval  14414  joindm  15172  meetdm  15186  gaorb  15824  efgcpbllema  16250  frgpuplem  16268  ltbval  17552  ltbwe  17553  opsrle  17556  opsrtoslem1  17564  opsrtoslem2  17565  dvdsrzring  17900  dvdsrz  17901  pjfval2  18133  lmfval  18835  lmbr  18861  cnmptid  19233  lgsquadlem3  22694  axcontlem2  23210  wlks  23424  trls  23434  dfconngra1  23556  dfadj2  25288  dmadjss  25290  cnvadj  25295  mpt2mptxf  25994  dfid4  27381  fneer  28558  opropabco  28615  fgraphopab  29576  fgraphxp  29577  fmptsnd  30720  mpt2mptx2  30722  cmtfvalN  32853  cmtvalN  32854  cvrfval  32911  cvrval  32912  dicval2  34822