Theorem opabbii 5153

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

Syntax hints:   ↔ wb 206   = wceq 1542  {copab 5148

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-opab 5149

This theorem is referenced by:  mptv  5192  2rbropap  5512  dfid4  5520  fconstmpt  5686  xpundi  5693  xpundir  5694  inxpOLD  5781  csbcnv  5832  cnvco  5834  resopab  5993  opabresid  6009  cnvi  6099  cnvun  6100  cnvxp  6115  cnvcnv3  6146  coundi  6205  coundir  6206  mptun  6638  fvopab6  6976  fmptsng  7116  fmptsnd  7117  cbvoprab1  7447  cbvoprab12  7449  dmoprabss  7464  mpomptx  7473  resoprab  7478  elrnmpores  7498  ov6g  7524  1st2val  7963  2nd2val  7964  dfoprab3s  7999  dfoprab3  8000  dfoprab4  8001  opabn1stprc  8004  mptmpoopabbrd  8026  fsplit  8060  mapsncnv  8834  xpcomco  8998  marypha2lem2  9342  oemapso  9594  ttrclresv  9629  leweon  9924  r0weon  9925  compsscnv  10284  fpwwe  10560  ltrelxr  11197  ltxrlt  11207  ltxr  13057  shftidt2  15034  prdsle  17416  prdsless  17417  prdsleval  17431  dfiso2  17730  joindm  18330  meetdm  18344  gaorb  19273  efgcpbllema  19720  frgpuplem  19738  dvdsrzring  21451  pjfval2  21699  ltbval  22031  ltbwe  22032  opsrle  22035  opsrtoslem1  22043  opsrtoslem2  22044  lmfval  23207  lmbr  23233  lgsquadlem3  27359  perpln1  28792  outpasch  28837  ishpg  28841  axcontlem2  29048  wksfval  29693  wlkson  29738  pthsfval  29802  ispth  29804  dfadj2  31971  dmadjss  31973  cnvadj  31978  mpomptxf  32766  lsmsnorb2  33467  satfv0  35556  satfvsuclem1  35557  satfvsuclem2  35558  satfbrsuc  35564  satf0  35570  satf0suclem  35573  fmlasuc0  35582  dfsuccf2  36139  fneer  36551  bj-dfmpoa  37446  bj-mpomptALT  37447  bj-brab2a1  37479  bj-imdiridlem  37515  bj-opabco  37518  opropabco  38059  xpv  38597  cnvepres  38639  inxp2  38710  disjecxrn  38747  xrninxp  38750  xrninxp2  38751  rnxrnres  38757  rnxrncnvepres  38758  rnxrnidres  38759  blockadjliftmap  38793  dfsucmap3  38798  dfsucmap4  38800  dfcoss2  38838  dfcoss3  38839  cosscnv  38841  coss1cnvres  38842  coss2cnvepres  38843  1cossres  38854  dfcoels  38855  ressn2  38867  br1cosscnvxrn  38899  1cosscnvxrn  38900  coss0  38904  cossid  38905  dfssr2  38914  dfpetparts2  39307  dfpeters2  39309  petseq  39311  cmtfvalN  39670  cmtvalN  39671  cvrfval  39728  cvrval  39729  dicval2  41639  aks6d1c1p1rcl  42561  aks6d1c1rh  42578  fgraphopab  43649  fgraphxp  43650  modelaxreplem2  45424  mptssid  45688  dfnelbr2  47733  opabbrfex0d  47746  opabbrfexd  47748  upwlksfval  48623  xpsnopab  48645  mpomptx2  48823  upfval2  49664