Theorem opabbii 5214

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

Syntax hints:   ↔ wb 206   = wceq 1536  {copab 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-opab 5210

This theorem is referenced by:  mptv  5263  2rbropap  5575  dfid4  5583  fconstmpt  5750  xpundi  5756  xpundir  5757  inxpOLD  5845  csbcnv  5896  cnvco  5898  resopab  6053  opabresid  6069  cnvi  6163  cnvun  6164  cnvxp  6178  cnvcnv3  6209  coundi  6268  coundir  6269  mptun  6714  fvopab6  7049  fmptsng  7187  fmptsnd  7188  cbvoprab1  7519  cbvoprab12  7521  dmoprabss  7535  mpomptx  7545  resoprab  7550  elrnmpores  7570  ov6g  7596  1st2val  8040  2nd2val  8041  dfoprab3s  8076  dfoprab3  8077  dfoprab4  8078  opabn1stprc  8081  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  fsplit  8140  mapsncnv  8931  xpcomco  9100  marypha2lem2  9473  oemapso  9719  ttrclresv  9754  leweon  10048  r0weon  10049  compsscnv  10408  fpwwe  10683  ltrelxr  11319  ltxrlt  11328  ltxr  13154  shftidt2  15116  prdsle  17508  prdsless  17509  prdsleval  17523  dfiso2  17819  joindm  18432  meetdm  18446  gaorb  19337  efgcpbllema  19786  frgpuplem  19804  dvdsrzring  21489  pjfval2  21746  ltbval  22078  ltbwe  22079  opsrle  22082  opsrtoslem1  22096  opsrtoslem2  22097  lmfval  23255  lmbr  23281  lgsquadlem3  27440  perpln1  28732  outpasch  28777  ishpg  28781  axcontlem2  28994  wksfval  29641  wlkson  29688  pthsfval  29753  ispth  29755  dfadj2  31913  dmadjss  31915  cnvadj  31920  mpomptxf  32693  lsmsnorb2  33399  satfv0  35342  satfvsuclem1  35343  satfvsuclem2  35344  satfbrsuc  35350  satf0  35356  satf0suclem  35359  fmlasuc0  35368  fneer  36335  bj-dfmpoa  37100  bj-mpomptALT  37101  bj-brab2a1  37131  bj-imdiridlem  37167  bj-opabco  37170  opropabco  37710  cnvepres  38279  inxp2  38348  disjecxrn  38370  xrninxp  38373  xrninxp2  38374  rnxrnres  38380  rnxrncnvepres  38381  rnxrnidres  38382  dfcoss2  38394  dfcoss3  38395  cosscnv  38397  coss1cnvres  38398  coss2cnvepres  38399  1cossres  38410  dfcoels  38411  ressn2  38423  br1cosscnvxrn  38455  1cosscnvxrn  38456  coss0  38460  cossid  38461  dfssr2  38480  cmtfvalN  39191  cmtvalN  39192  cvrfval  39249  cvrval  39250  dicval2  41161  aks6d1c1p1rcl  42089  aks6d1c1rh  42106  fgraphopab  43191  fgraphxp  43192  modelaxreplem2  44943  mptssid  45184  dfnelbr2  47222  opabbrfex0d  47235  opabbrfexd  47237  upwlksfval  47978  xpsnopab  48000  mpomptx2  48179