Theorem opabbii 5176

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-opab 5172

This theorem is referenced by:  mptv  5215  2rbropap  5528  dfid4  5536  fconstmpt  5702  xpundi  5709  xpundir  5710  inxpOLD  5798  csbcnv  5849  cnvco  5851  resopab  6007  opabresid  6023  cnvi  6116  cnvun  6117  cnvxp  6132  cnvcnv3  6163  coundi  6222  coundir  6223  mptun  6666  fvopab6  7004  fmptsng  7144  fmptsnd  7145  cbvoprab1  7478  cbvoprab12  7480  dmoprabss  7495  mpomptx  7504  resoprab  7509  elrnmpores  7529  ov6g  7555  1st2val  7998  2nd2val  7999  dfoprab3s  8034  dfoprab3  8035  dfoprab4  8036  opabn1stprc  8039  mptmpoopabbrd  8061  mptmpoopabbrdOLD  8062  mptmpoopabbrdOLDOLD  8064  fsplit  8098  mapsncnv  8868  xpcomco  9035  marypha2lem2  9393  oemapso  9641  ttrclresv  9676  leweon  9970  r0weon  9971  compsscnv  10330  fpwwe  10605  ltrelxr  11241  ltxrlt  11250  ltxr  13081  shftidt2  15053  prdsle  17431  prdsless  17432  prdsleval  17446  dfiso2  17740  joindm  18340  meetdm  18354  gaorb  19245  efgcpbllema  19690  frgpuplem  19708  dvdsrzring  21377  pjfval2  21624  ltbval  21956  ltbwe  21957  opsrle  21960  opsrtoslem1  21968  opsrtoslem2  21969  lmfval  23125  lmbr  23151  lgsquadlem3  27299  perpln1  28643  outpasch  28688  ishpg  28692  axcontlem2  28898  wksfval  29543  wlkson  29590  pthsfval  29655  ispth  29657  dfadj2  31820  dmadjss  31822  cnvadj  31827  mpomptxf  32607  lsmsnorb2  33369  satfv0  35345  satfvsuclem1  35346  satfvsuclem2  35347  satfbrsuc  35353  satf0  35359  satf0suclem  35362  fmlasuc0  35371  fneer  36336  bj-dfmpoa  37101  bj-mpomptALT  37102  bj-brab2a1  37132  bj-imdiridlem  37168  bj-opabco  37171  opropabco  37713  cnvepres  38281  inxp2  38344  disjecxrn  38370  xrninxp  38373  xrninxp2  38374  rnxrnres  38380  rnxrncnvepres  38381  rnxrnidres  38382  dfcoss2  38399  dfcoss3  38400  cosscnv  38402  coss1cnvres  38403  coss2cnvepres  38404  1cossres  38415  dfcoels  38416  ressn2  38428  br1cosscnvxrn  38460  1cosscnvxrn  38461  coss0  38465  cossid  38466  dfssr2  38485  cmtfvalN  39198  cmtvalN  39199  cvrfval  39256  cvrval  39257  dicval2  41168  aks6d1c1p1rcl  42091  aks6d1c1rh  42108  fgraphopab  43185  fgraphxp  43186  modelaxreplem2  44962  mptssid  45228  dfnelbr2  47264  opabbrfex0d  47277  opabbrfexd  47279  upwlksfval  48113  xpsnopab  48135  mpomptx2  48313  upfval2  49156