Theorem opabbii 5124

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

Syntax hints:   ↔ wb 208   = wceq 1531  {copab 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-opab 5120

This theorem is referenced by:  mptv  5162  2rbropap  5442  dfid4  5454  fconstmpt  5607  xpundi  5613  xpundir  5614  inxp  5696  csbcnv  5747  cnvco  5749  resopab  5895  opabresid  5910  opabresidOLD  5912  cnvi  5993  cnvun  5994  cnvxp  6007  cnvcnv3  6038  coundi  6093  coundir  6094  mptun  6487  fvopab6  6794  fmptsng  6923  fmptsnd  6924  cbvoprab1  7233  cbvoprab12  7235  dmoprabss  7248  mpomptx  7257  resoprab  7262  elrnmpores  7280  ov6g  7304  1st2val  7709  2nd2val  7710  dfoprab3s  7743  dfoprab3  7744  dfoprab4  7745  opabn1stprc  7748  mptmpoopabbrd  7770  fsplit  7804  fsplitOLD  7805  mapsncnv  8449  xpcomco  8599  marypha2lem2  8892  oemapso  9137  leweon  9429  r0weon  9430  compsscnv  9785  fpwwe  10060  ltrelxr  10694  ltxrlt  10703  ltxr  12502  shftidt2  14432  prdsle  16727  prdsless  16728  prdsleval  16742  dfiso2  17034  joindm  17605  meetdm  17619  gaorb  18429  efgcpbllema  18872  frgpuplem  18890  ltbval  20244  ltbwe  20245  opsrle  20248  opsrtoslem1  20256  opsrtoslem2  20257  dvdsrzring  20622  pjfval2  20845  lmfval  21832  lmbr  21858  lgsquadlem3  25950  perpln1  26488  outpasch  26533  ishpg  26537  axcontlem2  26743  wksfval  27383  wlkson  27430  pthsfval  27494  ispth  27496  dfadj2  29654  dmadjss  29656  cnvadj  29661  mpomptxf  30417  satfv0  32598  satfvsuclem1  32599  satfvsuclem2  32600  satfbrsuc  32606  satf0  32612  satf0suclem  32615  fmlasuc0  32624  fneer  33694  bj-dfmpoa  34402  bj-mpomptALT  34403  bj-brab2a1  34433  opropabco  34991  cnvepres  35547  inxp2  35611  xrninxp  35632  xrninxp2  35633  rnxrnres  35639  rnxrncnvepres  35640  rnxrnidres  35641  dfcoss2  35653  dfcoss3  35654  1cossres  35666  dfcoels  35667  br1cosscnvxrn  35706  1cosscnvxrn  35707  coss0  35711  cossid  35712  dfssr2  35731  cmtfvalN  36338  cmtvalN  36339  cvrfval  36396  cvrval  36397  dicval2  38307  fgraphopab  39801  fgraphxp  39802  mptssid  41501  dfnelbr2  43463  opabbrfex0d  43476  opabbrfexd  43478  upwlksfval  44001  xpsnopab  44023  mpomptx2  44374