Theorem opabbii 5210

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 5209	. 2 ⊢ (𝑧 = 𝑧 → {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓})
5	1, 4	ax-mp 5	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓}

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-opab 5206

This theorem is referenced by:  mptv  5258  2rbropap  5571  dfid4  5579  fconstmpt  5747  xpundi  5754  xpundir  5755  inxpOLD  5843  csbcnv  5894  cnvco  5896  resopab  6052  opabresid  6068  cnvi  6161  cnvun  6162  cnvxp  6177  cnvcnv3  6208  coundi  6267  coundir  6268  mptun  6714  fvopab6  7050  fmptsng  7188  fmptsnd  7189  cbvoprab1  7520  cbvoprab12  7522  dmoprabss  7537  mpomptx  7546  resoprab  7551  elrnmpores  7571  ov6g  7597  1st2val  8042  2nd2val  8043  dfoprab3s  8078  dfoprab3  8079  dfoprab4  8080  opabn1stprc  8083  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabbrdOLDOLD  8108  fsplit  8142  mapsncnv  8933  xpcomco  9102  marypha2lem2  9476  oemapso  9722  ttrclresv  9757  leweon  10051  r0weon  10052  compsscnv  10411  fpwwe  10686  ltrelxr  11322  ltxrlt  11331  ltxr  13157  shftidt2  15120  prdsle  17507  prdsless  17508  prdsleval  17522  dfiso2  17816  joindm  18420  meetdm  18434  gaorb  19325  efgcpbllema  19772  frgpuplem  19790  dvdsrzring  21472  pjfval2  21729  ltbval  22061  ltbwe  22062  opsrle  22065  opsrtoslem1  22079  opsrtoslem2  22080  lmfval  23240  lmbr  23266  lgsquadlem3  27426  perpln1  28718  outpasch  28763  ishpg  28767  axcontlem2  28980  wksfval  29627  wlkson  29674  pthsfval  29739  ispth  29741  dfadj2  31904  dmadjss  31906  cnvadj  31911  mpomptxf  32687  lsmsnorb2  33420  satfv0  35363  satfvsuclem1  35364  satfvsuclem2  35365  satfbrsuc  35371  satf0  35377  satf0suclem  35380  fmlasuc0  35389  fneer  36354  bj-dfmpoa  37119  bj-mpomptALT  37120  bj-brab2a1  37150  bj-imdiridlem  37186  bj-opabco  37189  opropabco  37731  cnvepres  38299  inxp2  38368  disjecxrn  38390  xrninxp  38393  xrninxp2  38394  rnxrnres  38400  rnxrncnvepres  38401  rnxrnidres  38402  dfcoss2  38414  dfcoss3  38415  cosscnv  38417  coss1cnvres  38418  coss2cnvepres  38419  1cossres  38430  dfcoels  38431  ressn2  38443  br1cosscnvxrn  38475  1cosscnvxrn  38476  coss0  38480  cossid  38481  dfssr2  38500  cmtfvalN  39211  cmtvalN  39212  cvrfval  39269  cvrval  39270  dicval2  41181  aks6d1c1p1rcl  42109  aks6d1c1rh  42126  fgraphopab  43215  fgraphxp  43216  modelaxreplem2  44996  mptssid  45247  dfnelbr2  47285  opabbrfex0d  47298  opabbrfexd  47300  upwlksfval  48051  xpsnopab  48073  mpomptx2  48251  upfval2  48934