Theorem opabbii 5215

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

Syntax hints:   ↔ wb 205   = wceq 1541  {copab 5210

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-opab 5211

This theorem is referenced by:  mptv  5264  2rbropap  5566  dfid4  5575  fconstmpt  5738  xpundi  5744  xpundir  5745  inxp  5832  csbcnv  5883  cnvco  5885  resopab  6034  opabresid  6049  cnvi  6141  cnvun  6142  cnvxp  6156  cnvcnv3  6187  coundi  6246  coundir  6247  mptun  6696  fvopab6  7031  fmptsng  7168  fmptsnd  7169  cbvoprab1  7498  cbvoprab12  7500  dmoprabss  7513  mpomptx  7523  resoprab  7528  elrnmpores  7548  ov6g  7573  1st2val  8005  2nd2val  8006  dfoprab3s  8041  dfoprab3  8042  dfoprab4  8043  opabn1stprc  8046  mptmpoopabbrd  8069  mptmpoopabbrdOLD  8071  fsplit  8105  mapsncnv  8889  xpcomco  9064  marypha2lem2  9433  oemapso  9679  ttrclresv  9714  leweon  10008  r0weon  10009  compsscnv  10368  fpwwe  10643  ltrelxr  11279  ltxrlt  11288  ltxr  13099  shftidt2  15032  prdsle  17412  prdsless  17413  prdsleval  17427  dfiso2  17723  joindm  18332  meetdm  18346  gaorb  19212  efgcpbllema  19663  frgpuplem  19681  dvdsrzring  21232  pjfval2  21483  ltbval  21817  ltbwe  21818  opsrle  21821  opsrtoslem1  21835  opsrtoslem2  21836  lmfval  22956  lmbr  22982  lgsquadlem3  27109  perpln1  28216  outpasch  28261  ishpg  28265  axcontlem2  28478  wksfval  29121  wlkson  29168  pthsfval  29233  ispth  29235  dfadj2  31393  dmadjss  31395  cnvadj  31400  mpomptxf  32160  lsmsnorb2  32764  satfv0  34635  satfvsuclem1  34636  satfvsuclem2  34637  satfbrsuc  34643  satf0  34649  satf0suclem  34652  fmlasuc0  34661  fneer  35541  bj-dfmpoa  36302  bj-mpomptALT  36303  bj-brab2a1  36333  bj-imdiridlem  36369  bj-opabco  36372  opropabco  36895  cnvepres  37470  inxp2  37539  disjecxrn  37562  xrninxp  37565  xrninxp2  37566  rnxrnres  37572  rnxrncnvepres  37573  rnxrnidres  37574  dfcoss2  37586  dfcoss3  37587  cosscnv  37589  coss1cnvres  37590  coss2cnvepres  37591  1cossres  37602  dfcoels  37603  ressn2  37615  br1cosscnvxrn  37647  1cosscnvxrn  37648  coss0  37652  cossid  37653  dfssr2  37672  cmtfvalN  38383  cmtvalN  38384  cvrfval  38441  cvrval  38442  dicval2  40353  fgraphopab  42254  fgraphxp  42255  mptssid  44243  dfnelbr2  46280  opabbrfex0d  46293  opabbrfexd  46295  upwlksfval  46812  xpsnopab  46834  mpomptx2  47099