Theorem opabbii 5178

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {copab 5173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-opab 5174

This theorem is used by:  mptv  5217  2rbropap  5546  dfid4  5554  fconstmpt  5720  xpundi  5727  xpundir  5728  cnvi  5875  csbcnv  5876  csbcnvOLD  5877  cnvco  5879  resopab  6044  opabresid  6060  cnvun  6151  cnvxpOLD  6166  cnvcnv3  6198  coundi  6267  coundir  6268  mptun  6715  fvopab6  7059  fmptsng  7204  fmptsnd  7205  cbvoprab1  7538  cbvoprab12  7540  dmoprabss  7555  mpomptx  7564  resoprab  7569  elrnmpores  7590  ov6g  7616  mpt3mpt  7717  mpt3fvd  7720  1st2val  8063  2nd2val  8064  dfoprab3s  8099  dfoprab3  8100  dfoprab4  8101  opabn1stprc  8104  mptmpoopabbrd  8129  fsplit  8165  mapsncnv  8959  xpcomco  9124  marypha2lem2  9465  oemapso  9720  ttrclresv  9755  leweon  10129  r0weon  10130  compsscnv  10488  fpwwe  10770  ltrelxr  11409  ltxrlt  11419  ltxr  13284  shftidt2  15277  prdsle  17683  prdsless  17684  prdsleval  17698  dfiso2  17997  joindm  18597  meetdm  18611  gaorb  19572  efgcpbllema  20019  frgpuplem  20037  dvdsrzring  21822  pjfval2  22070  ltbval  22407  ltbwe  22408  opsrle  22411  opsrtoslem1  22419  opsrtoslem2  22420  lmfval  23605  lmbr  23631  lgsquadlem3  27766  perpln1  29242  outpasch  29290  ishpg  29294  tgaaddcpbllem2  29407  tgaaddcpbllem3  29408  tgaltai  29502  axcontlem2  29600  wksfval  30247  wlkson  30292  pthsfval  30361  ispth  30363  dfadj2  32544  dmadjss  32546  cnvadj  32551  mpomptxf  33369  lsmsnorb2  34051  mpofvd  35838  onf1we  35844  werankwe  35862  werankwe2  35863  dmr0ss  36043  dfk12  36053  dfk22  36054  dfk32  36055  satfv0  36331  satfvsuclem1  36332  satfvsuclem2  36333  satfbrsuc  36339  satf0  36345  satf0suclem  36348  fmlasuc0  36357  dfsuccf2  36920  fneer  37356  relpart  38186  coi1res  38199  coi2res  38200  coresrn  38204  bj-dfmpoa  38310  bj-mpomptALT  38311  bj-brab2a1  38338  bj-imdiridlem  38374  bj-opabco  38377  opropabco  38926  xpv  39460  cnvepres  39502  inxp2  39573  disjecxrn  39610  xrninxp  39613  xrninxp2  39614  rnxrnres  39620  rnxrncnvepres  39621  rnxrnidres  39622  blockadjliftmap  39656  dfsucmap3  39661  dfsucmap4  39663  dfcoss2  39701  dfcoss3  39702  cosscnv  39704  coss1cnvres  39705  coss2cnvepres  39706  1cossres  39717  dfcoels  39718  ressn2  39730  br1cosscnvxrn  39762  1cosscnvxrn  39763  coss0  39767  cossid  39768  dfssr2  39777  dfpetparts2  40170  dfpeters2  40172  petseq  40174  cmtfvalN  40533  cmtvalN  40534  cvrfval  40591  cvrval  40592  dicval2  42502  aks6d1c1p1rcl  43424  aks6d1c1rh  43441  fgraphopab  44466  fgraphxp  44467  modelaxreplem2  46233  mptssid  46526  dfnelbr2  48616  opabbrfex0d  48629  opabbrfexd  48631  upwlksfval  49506  xpsnopab  49528  mpomptx2  49778  upfval2  50624