Theorem opabbii 5141

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

Hypothesis

Ref	Expression
opabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
opabbii	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Proof of Theorem opabbii

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 11	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 5140	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 205   = wceq 1539  {copab 5136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-opab 5137

This theorem is referenced by:  mptv  5190  2rbropap  5479  dfid4  5490  fconstmpt  5649  xpundi  5655  xpundir  5656  inxp  5741  csbcnv  5792  cnvco  5794  resopab  5942  opabresid  5957  opabresidOLD  5959  cnvi  6045  cnvun  6046  cnvxp  6060  cnvcnv3  6091  coundi  6151  coundir  6152  mptun  6579  fvopab6  6908  fmptsng  7040  fmptsnd  7041  cbvoprab1  7362  cbvoprab12  7364  dmoprabss  7377  mpomptx  7387  resoprab  7392  elrnmpores  7411  ov6g  7436  1st2val  7859  2nd2val  7860  dfoprab3s  7893  dfoprab3  7894  dfoprab4  7895  opabn1stprc  7898  mptmpoopabbrd  7921  mptmpoopabbrdOLD  7923  fsplit  7957  fsplitOLD  7958  mapsncnv  8681  xpcomco  8849  marypha2lem2  9195  oemapso  9440  ttrclresv  9475  leweon  9767  r0weon  9768  compsscnv  10127  fpwwe  10402  ltrelxr  11036  ltxrlt  11045  ltxr  12851  shftidt2  14792  prdsle  17173  prdsless  17174  prdsleval  17188  dfiso2  17484  joindm  18093  meetdm  18107  gaorb  18913  efgcpbllema  19360  frgpuplem  19378  dvdsrzring  20683  pjfval2  20916  ltbval  21244  ltbwe  21245  opsrle  21248  opsrtoslem1  21262  opsrtoslem2  21263  lmfval  22383  lmbr  22409  lgsquadlem3  26530  perpln1  27071  outpasch  27116  ishpg  27120  axcontlem2  27333  wksfval  27976  wlkson  28024  pthsfval  28089  ispth  28091  dfadj2  30247  dmadjss  30249  cnvadj  30254  mpomptxf  31016  lsmsnorb2  31580  satfv0  33320  satfvsuclem1  33321  satfvsuclem2  33322  satfbrsuc  33328  satf0  33334  satf0suclem  33337  fmlasuc0  33346  fneer  34542  bj-dfmpoa  35289  bj-mpomptALT  35290  bj-brab2a1  35320  bj-imdiridlem  35356  bj-opabco  35359  opropabco  35882  cnvepres  36433  inxp2  36497  xrninxp  36518  xrninxp2  36519  rnxrnres  36525  rnxrncnvepres  36526  rnxrnidres  36527  dfcoss2  36539  dfcoss3  36540  1cossres  36552  dfcoels  36553  br1cosscnvxrn  36592  1cosscnvxrn  36593  coss0  36597  cossid  36598  dfssr2  36617  cmtfvalN  37224  cmtvalN  37225  cvrfval  37282  cvrval  37283  dicval2  39193  fgraphopab  41035  fgraphxp  41036  mptssid  42785  dfnelbr2  44765  opabbrfex0d  44778  opabbrfexd  44780  upwlksfval  45297  xpsnopab  45319  mpomptx2  45670