Theorem opabbii 5186

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-opab 5182

This theorem is referenced by:  mptv  5228  2rbropap  5541  dfid4  5549  fconstmpt  5716  xpundi  5723  xpundir  5724  inxpOLD  5812  csbcnv  5863  cnvco  5865  resopab  6021  opabresid  6037  cnvi  6130  cnvun  6131  cnvxp  6146  cnvcnv3  6177  coundi  6236  coundir  6237  mptun  6683  fvopab6  7019  fmptsng  7159  fmptsnd  7160  cbvoprab1  7492  cbvoprab12  7494  dmoprabss  7509  mpomptx  7518  resoprab  7523  elrnmpores  7543  ov6g  7569  1st2val  8014  2nd2val  8015  dfoprab3s  8050  dfoprab3  8051  dfoprab4  8052  opabn1stprc  8055  mptmpoopabbrd  8077  mptmpoopabbrdOLD  8078  mptmpoopabbrdOLDOLD  8080  fsplit  8114  mapsncnv  8905  xpcomco  9074  marypha2lem2  9446  oemapso  9694  ttrclresv  9729  leweon  10023  r0weon  10024  compsscnv  10383  fpwwe  10658  ltrelxr  11294  ltxrlt  11303  ltxr  13129  shftidt2  15098  prdsle  17474  prdsless  17475  prdsleval  17489  dfiso2  17783  joindm  18383  meetdm  18397  gaorb  19288  efgcpbllema  19733  frgpuplem  19751  dvdsrzring  21420  pjfval2  21667  ltbval  21999  ltbwe  22000  opsrle  22003  opsrtoslem1  22011  opsrtoslem2  22012  lmfval  23168  lmbr  23194  lgsquadlem3  27343  perpln1  28635  outpasch  28680  ishpg  28684  axcontlem2  28890  wksfval  29535  wlkson  29582  pthsfval  29647  ispth  29649  dfadj2  31812  dmadjss  31814  cnvadj  31819  mpomptxf  32601  lsmsnorb2  33353  satfv0  35326  satfvsuclem1  35327  satfvsuclem2  35328  satfbrsuc  35334  satf0  35340  satf0suclem  35343  fmlasuc0  35352  fneer  36317  bj-dfmpoa  37082  bj-mpomptALT  37083  bj-brab2a1  37113  bj-imdiridlem  37149  bj-opabco  37152  opropabco  37694  cnvepres  38262  inxp2  38331  disjecxrn  38353  xrninxp  38356  xrninxp2  38357  rnxrnres  38363  rnxrncnvepres  38364  rnxrnidres  38365  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  39174  cmtvalN  39175  cvrfval  39232  cvrval  39233  dicval2  41144  aks6d1c1p1rcl  42067  aks6d1c1rh  42084  fgraphopab  43174  fgraphxp  43175  modelaxreplem2  44952  mptssid  45213  dfnelbr2  47250  opabbrfex0d  47263  opabbrfexd  47265  upwlksfval  48058  xpsnopab  48080  mpomptx2  48258  upfval2  49060