Theorem opabbii 5172

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-opab 5168

This theorem is used by:  mptv  5211  2rbropap  5543  dfid4  5551  fconstmpt  5717  xpundi  5724  xpundir  5725  cnvi  5865  csbcnv  5866  csbcnvOLD  5867  cnvco  5869  resopab  6030  opabresid  6046  cnvun  6133  cnvxpOLD  6149  cnvcnv3  6181  coundi  6243  coundir  6244  mptun  6678  fvopab6  7021  fmptsng  7166  fmptsnd  7167  cbvoprab1  7500  cbvoprab12  7502  dmoprabss  7517  mpomptx  7526  resoprab  7531  elrnmpores  7551  ov6g  7577  1st2val  8014  2nd2val  8015  dfoprab3s  8050  dfoprab3  8051  dfoprab4  8052  opabn1stprc  8055  mptmpoopabbrd  8080  fsplit  8114  mapsncnv  8900  xpcomco  9065  marypha2lem2  9406  oemapso  9661  ttrclresv  9696  leweon  10014  r0weon  10015  compsscnv  10373  fpwwe  10655  ltrelxr  11294  ltxrlt  11304  ltxr  13166  shftidt2  15154  prdsle  17547  prdsless  17548  prdsleval  17562  dfiso2  17861  joindm  18461  meetdm  18475  gaorb  19434  efgcpbllema  19881  frgpuplem  19899  dvdsrzring  21674  pjfval2  21922  ltbval  22259  ltbwe  22260  opsrle  22263  opsrtoslem1  22271  opsrtoslem2  22272  lmfval  23457  lmbr  23483  lgsquadlem3  27618  perpln1  29064  outpasch  29112  ishpg  29116  tgaaddcpbllem2  29229  tgaaddcpbllem3  29230  tgaltai  29324  axcontlem2  29422  wksfval  30069  wlkson  30114  pthsfval  30183  ispth  30185  dfadj2  32366  dmadjss  32368  cnvadj  32373  mpomptxf  33151  lsmsnorb2  33825  satfv0  35937  satfvsuclem1  35938  satfvsuclem2  35939  satfbrsuc  35945  satf0  35951  satf0suclem  35954  fmlasuc0  35963  dfsuccf2  36520  fneer  36972  bj-dfmpoa  37868  bj-mpomptALT  37869  bj-brab2a1  37901  bj-imdiridlem  37937  bj-opabco  37940  opropabco  38474  xpv  39010  cnvepres  39052  inxp2  39123  disjecxrn  39160  xrninxp  39163  xrninxp2  39164  rnxrnres  39170  rnxrncnvepres  39171  rnxrnidres  39172  blockadjliftmap  39206  dfsucmap3  39211  dfsucmap4  39213  dfcoss2  39251  dfcoss3  39252  cosscnv  39254  coss1cnvres  39255  coss2cnvepres  39256  1cossres  39267  dfcoels  39268  ressn2  39280  br1cosscnvxrn  39312  1cosscnvxrn  39313  coss0  39317  cossid  39318  dfssr2  39327  dfpetparts2  39720  dfpeters2  39722  petseq  39724  cmtfvalN  40083  cmtvalN  40084  cvrfval  40141  cvrval  40142  dicval2  42052  aks6d1c1p1rcl  42974  aks6d1c1rh  42991  fgraphopab  44044  fgraphxp  44045  modelaxreplem2  45802  mptssid  46070  dfnelbr2  48161  opabbrfex0d  48174  opabbrfexd  48176  upwlksfval  49051  xpsnopab  49073  mpomptx2  49265  upfval2  50103