Theorem opabbii 5169

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

Syntax hints:   ↔ wb 206   = wceq 1540  {copab 5164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-opab 5165

This theorem is referenced by:  mptv  5208  2rbropap  5519  dfid4  5527  fconstmpt  5693  xpundi  5700  xpundir  5701  inxpOLD  5786  csbcnv  5837  cnvco  5839  resopab  5994  opabresid  6010  cnvi  6102  cnvun  6103  cnvxp  6118  cnvcnv3  6149  coundi  6208  coundir  6209  mptun  6646  fvopab6  6984  fmptsng  7124  fmptsnd  7125  cbvoprab1  7456  cbvoprab12  7458  dmoprabss  7473  mpomptx  7482  resoprab  7487  elrnmpores  7507  ov6g  7533  1st2val  7975  2nd2val  7976  dfoprab3s  8011  dfoprab3  8012  dfoprab4  8013  opabn1stprc  8016  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  fsplit  8073  mapsncnv  8843  xpcomco  9008  marypha2lem2  9363  oemapso  9611  ttrclresv  9646  leweon  9940  r0weon  9941  compsscnv  10300  fpwwe  10575  ltrelxr  11211  ltxrlt  11220  ltxr  13051  shftidt2  15023  prdsle  17401  prdsless  17402  prdsleval  17416  dfiso2  17710  joindm  18310  meetdm  18324  gaorb  19215  efgcpbllema  19660  frgpuplem  19678  dvdsrzring  21347  pjfval2  21594  ltbval  21926  ltbwe  21927  opsrle  21930  opsrtoslem1  21938  opsrtoslem2  21939  lmfval  23095  lmbr  23121  lgsquadlem3  27269  perpln1  28613  outpasch  28658  ishpg  28662  axcontlem2  28868  wksfval  29513  wlkson  29558  pthsfval  29622  ispth  29624  dfadj2  31787  dmadjss  31789  cnvadj  31794  mpomptxf  32574  lsmsnorb2  33336  satfv0  35318  satfvsuclem1  35319  satfvsuclem2  35320  satfbrsuc  35326  satf0  35332  satf0suclem  35335  fmlasuc0  35344  fneer  36314  bj-dfmpoa  37079  bj-mpomptALT  37080  bj-brab2a1  37110  bj-imdiridlem  37146  bj-opabco  37149  opropabco  37691  cnvepres  38259  inxp2  38322  disjecxrn  38348  xrninxp  38351  xrninxp2  38352  rnxrnres  38358  rnxrncnvepres  38359  rnxrnidres  38360  dfcoss2  38377  dfcoss3  38378  cosscnv  38380  coss1cnvres  38381  coss2cnvepres  38382  1cossres  38393  dfcoels  38394  ressn2  38406  br1cosscnvxrn  38438  1cosscnvxrn  38439  coss0  38443  cossid  38444  dfssr2  38463  cmtfvalN  39176  cmtvalN  39177  cvrfval  39234  cvrval  39235  dicval2  41146  aks6d1c1p1rcl  42069  aks6d1c1rh  42086  fgraphopab  43165  fgraphxp  43166  modelaxreplem2  44942  mptssid  45208  dfnelbr2  47247  opabbrfex0d  47260  opabbrfexd  47262  upwlksfval  48096  xpsnopab  48118  mpomptx2  48296  upfval2  49139