Theorem opabbii 5135

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 2823	. 2 ⊢ 𝑧 = 𝑧
2		opabbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
3	2	a1i 11	. . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓))
4	3	opabbidv 5134	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Syntax hints:   ↔ wb 208   = wceq 1537  {copab 5130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-opab 5131

This theorem is referenced by:  mptv  5173  2rbropap  5453  dfid4  5463  fconstmpt  5616  xpundi  5622  xpundir  5623  inxp  5705  csbcnv  5756  cnvco  5758  resopab  5904  opabresid  5919  opabresidOLD  5921  cnvi  6002  cnvun  6003  cnvxp  6016  cnvcnv3  6047  coundi  6102  coundir  6103  mptun  6496  fvopab6  6803  fmptsng  6932  fmptsnd  6933  cbvoprab1  7243  cbvoprab12  7245  dmoprabss  7258  mpomptx  7267  resoprab  7272  elrnmpores  7290  ov6g  7314  1st2val  7719  2nd2val  7720  dfoprab3s  7753  dfoprab3  7754  dfoprab4  7755  opabn1stprc  7758  mptmpoopabbrd  7780  fsplit  7814  fsplitOLD  7815  mapsncnv  8459  xpcomco  8609  marypha2lem2  8902  oemapso  9147  leweon  9439  r0weon  9440  compsscnv  9795  fpwwe  10070  ltrelxr  10704  ltxrlt  10713  ltxr  12513  shftidt2  14442  prdsle  16737  prdsless  16738  prdsleval  16752  dfiso2  17044  joindm  17615  meetdm  17629  gaorb  18439  efgcpbllema  18882  frgpuplem  18900  ltbval  20254  ltbwe  20255  opsrle  20258  opsrtoslem1  20266  opsrtoslem2  20267  dvdsrzring  20632  pjfval2  20855  lmfval  21842  lmbr  21868  lgsquadlem3  25960  perpln1  26498  outpasch  26543  ishpg  26547  axcontlem2  26753  wksfval  27393  wlkson  27440  pthsfval  27504  ispth  27506  dfadj2  29664  dmadjss  29666  cnvadj  29671  mpomptxf  30427  satfv0  32607  satfvsuclem1  32608  satfvsuclem2  32609  satfbrsuc  32615  satf0  32621  satf0suclem  32624  fmlasuc0  32633  fneer  33703  bj-dfmpoa  34412  bj-mpomptALT  34413  bj-brab2a1  34443  opropabco  35001  cnvepres  35557  inxp2  35621  xrninxp  35642  xrninxp2  35643  rnxrnres  35649  rnxrncnvepres  35650  rnxrnidres  35651  dfcoss2  35663  dfcoss3  35664  1cossres  35676  dfcoels  35677  br1cosscnvxrn  35716  1cosscnvxrn  35717  coss0  35721  cossid  35722  dfssr2  35741  cmtfvalN  36348  cmtvalN  36349  cvrfval  36406  cvrval  36407  dicval2  38317  fgraphopab  39817  fgraphxp  39818  mptssid  41518  dfnelbr2  43479  opabbrfex0d  43492  opabbrfexd  43494  upwlksfval  44017  xpsnopab  44039  mpomptx2  44390