Theorem opabbii 5097

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

Syntax hints:   ↔ wb 209   = wceq 1538  {copab 5092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-opab 5093

This theorem is referenced by:  mptv  5135  2rbropap  5416  dfid4  5426  fconstmpt  5578  xpundi  5584  xpundir  5585  inxp  5667  csbcnv  5718  cnvco  5720  resopab  5869  opabresid  5884  opabresidOLD  5886  cnvi  5967  cnvun  5968  cnvxp  5981  cnvcnv3  6012  coundi  6067  coundir  6068  mptun  6466  fvopab6  6778  fmptsng  6907  fmptsnd  6908  cbvoprab1  7220  cbvoprab12  7222  dmoprabss  7235  mpomptx  7244  resoprab  7249  elrnmpores  7267  ov6g  7292  1st2val  7699  2nd2val  7700  dfoprab3s  7733  dfoprab3  7734  dfoprab4  7735  opabn1stprc  7738  mptmpoopabbrd  7761  fsplit  7795  fsplitOLD  7796  mapsncnv  8440  xpcomco  8590  marypha2lem2  8884  oemapso  9129  leweon  9422  r0weon  9423  compsscnv  9782  fpwwe  10057  ltrelxr  10691  ltxrlt  10700  ltxr  12498  shftidt2  14432  prdsle  16727  prdsless  16728  prdsleval  16742  dfiso2  17034  joindm  17605  meetdm  17619  gaorb  18429  efgcpbllema  18872  frgpuplem  18890  dvdsrzring  20176  pjfval2  20398  ltbval  20711  ltbwe  20712  opsrle  20715  opsrtoslem1  20723  opsrtoslem2  20724  lmfval  21837  lmbr  21863  lgsquadlem3  25966  perpln1  26504  outpasch  26549  ishpg  26553  axcontlem2  26759  wksfval  27399  wlkson  27446  pthsfval  27510  ispth  27512  dfadj2  29668  dmadjss  29670  cnvadj  29675  mpomptxf  30442  satfv0  32718  satfvsuclem1  32719  satfvsuclem2  32720  satfbrsuc  32726  satf0  32732  satf0suclem  32735  fmlasuc0  32744  fneer  33814  bj-dfmpoa  34533  bj-mpomptALT  34534  bj-brab2a1  34564  bj-imdiridlem  34600  bj-opabco  34603  opropabco  35162  cnvepres  35715  inxp2  35779  xrninxp  35800  xrninxp2  35801  rnxrnres  35807  rnxrncnvepres  35808  rnxrnidres  35809  dfcoss2  35821  dfcoss3  35822  1cossres  35834  dfcoels  35835  br1cosscnvxrn  35874  1cosscnvxrn  35875  coss0  35879  cossid  35880  dfssr2  35899  cmtfvalN  36506  cmtvalN  36507  cvrfval  36564  cvrval  36565  dicval2  38475  fgraphopab  40154  fgraphxp  40155  mptssid  41877  dfnelbr2  43829  opabbrfex0d  43842  opabbrfexd  43844  upwlksfval  44363  xpsnopab  44385  mpomptx2  44736