Theorem opabbii 5216

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

Syntax hints:   ↔ wb 205   = wceq 1533  {copab 5211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-opab 5212

This theorem is referenced by:  mptv  5265  2rbropap  5568  dfid4  5577  fconstmpt  5740  xpundi  5746  xpundir  5747  inxpOLD  5835  csbcnv  5886  cnvco  5888  resopab  6039  opabresid  6054  cnvi  6148  cnvun  6149  cnvxp  6163  cnvcnv3  6194  coundi  6253  coundir  6254  mptun  6702  fvopab6  7038  fmptsng  7177  fmptsnd  7178  cbvoprab1  7507  cbvoprab12  7509  dmoprabss  7523  mpomptx  7533  resoprab  7538  elrnmpores  7559  ov6g  7585  1st2val  8022  2nd2val  8023  dfoprab3s  8058  dfoprab3  8059  dfoprab4  8060  opabn1stprc  8063  mptmpoopabbrd  8085  mptmpoopabbrdOLD  8086  mptmpoopabbrdOLDOLD  8088  fsplit  8122  mapsncnv  8912  xpcomco  9090  marypha2lem2  9466  oemapso  9712  ttrclresv  9747  leweon  10041  r0weon  10042  compsscnv  10401  fpwwe  10676  ltrelxr  11312  ltxrlt  11321  ltxr  13135  shftidt2  15069  prdsle  17452  prdsless  17453  prdsleval  17467  dfiso2  17763  joindm  18375  meetdm  18389  gaorb  19275  efgcpbllema  19726  frgpuplem  19744  dvdsrzring  21409  pjfval2  21665  ltbval  22008  ltbwe  22009  opsrle  22012  opsrtoslem1  22026  opsrtoslem2  22027  lmfval  23185  lmbr  23211  lgsquadlem3  27365  perpln1  28591  outpasch  28636  ishpg  28640  axcontlem2  28853  wksfval  29500  wlkson  29547  pthsfval  29612  ispth  29614  dfadj2  31772  dmadjss  31774  cnvadj  31779  mpomptxf  32550  lsmsnorb2  33209  satfv0  35101  satfvsuclem1  35102  satfvsuclem2  35103  satfbrsuc  35109  satf0  35115  satf0suclem  35118  fmlasuc0  35127  fneer  35970  bj-dfmpoa  36730  bj-mpomptALT  36731  bj-brab2a1  36761  bj-imdiridlem  36797  bj-opabco  36800  opropabco  37330  cnvepres  37902  inxp2  37971  disjecxrn  37993  xrninxp  37996  xrninxp2  37997  rnxrnres  38003  rnxrncnvepres  38004  rnxrnidres  38005  dfcoss2  38017  dfcoss3  38018  cosscnv  38020  coss1cnvres  38021  coss2cnvepres  38022  1cossres  38033  dfcoels  38034  ressn2  38046  br1cosscnvxrn  38078  1cosscnvxrn  38079  coss0  38083  cossid  38084  dfssr2  38103  cmtfvalN  38814  cmtvalN  38815  cvrfval  38872  cvrval  38873  dicval2  40784  aks6d1c1p1rcl  41713  aks6d1c1rh  41730  fgraphopab  42775  fgraphxp  42776  mptssid  44756  dfnelbr2  46793  opabbrfex0d  46806  opabbrfexd  46808  upwlksfval  47385  xpsnopab  47407  mpomptx2  47586