Theorem opabbii 5165

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

Syntax hints:   ↔ wb 206   = wceq 1541  {copab 5160

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 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-opab 5161

This theorem is referenced by:  mptv  5204  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  6975  fmptsng  7114  fmptsnd  7115  cbvoprab1  7445  cbvoprab12  7447  dmoprabss  7462  mpomptx  7471  resoprab  7476  elrnmpores  7496  ov6g  7522  1st2val  7961  2nd2val  7962  dfoprab3s  7997  dfoprab3  7998  dfoprab4  7999  opabn1stprc  8002  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  fsplit  8059  mapsncnv  8831  xpcomco  8995  marypha2lem2  9339  oemapso  9591  ttrclresv  9626  leweon  9921  r0weon  9922  compsscnv  10281  fpwwe  10557  ltrelxr  11193  ltxrlt  11203  ltxr  13029  shftidt2  15004  prdsle  17382  prdsless  17383  prdsleval  17397  dfiso2  17696  joindm  18296  meetdm  18310  gaorb  19236  efgcpbllema  19683  frgpuplem  19701  dvdsrzring  21416  pjfval2  21664  ltbval  21998  ltbwe  21999  opsrle  22002  opsrtoslem1  22010  opsrtoslem2  22011  lmfval  23176  lmbr  23202  lgsquadlem3  27349  perpln1  28782  outpasch  28827  ishpg  28831  axcontlem2  29038  wksfval  29683  wlkson  29728  pthsfval  29792  ispth  29794  dfadj2  31960  dmadjss  31962  cnvadj  31967  mpomptxf  32757  lsmsnorb2  33473  satfv0  35552  satfvsuclem1  35553  satfvsuclem2  35554  satfbrsuc  35560  satf0  35566  satf0suclem  35569  fmlasuc0  35578  dfsuccf2  36135  fneer  36547  bj-dfmpoa  37323  bj-mpomptALT  37324  bj-brab2a1  37354  bj-imdiridlem  37390  bj-opabco  37393  opropabco  37925  cnvepres  38497  inxp2  38560  disjecxrn  38597  xrninxp  38600  xrninxp2  38601  rnxrnres  38607  rnxrncnvepres  38608  rnxrnidres  38609  blockadjliftmap  38633  dfsucmap3  38637  dfsucmap4  38639  dfcoss2  38676  dfcoss3  38677  cosscnv  38679  coss1cnvres  38680  coss2cnvepres  38681  1cossres  38692  dfcoels  38693  ressn2  38705  br1cosscnvxrn  38737  1cosscnvxrn  38738  coss0  38742  cossid  38743  dfssr2  38752  dfblockliftfix2  38897  cmtfvalN  39470  cmtvalN  39471  cvrfval  39528  cvrval  39529  dicval2  41439  aks6d1c1p1rcl  42362  aks6d1c1rh  42379  fgraphopab  43445  fgraphxp  43446  modelaxreplem2  45220  mptssid  45485  dfnelbr2  47519  opabbrfex0d  47532  opabbrfexd  47534  upwlksfval  48381  xpsnopab  48403  mpomptx2  48581  upfval2  49422