Theorem opabbii 5233

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

Syntax hints:   ↔ wb 206   = wceq 1537  {copab 5228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-opab 5229

This theorem is referenced by:  mptv  5282  2rbropap  5585  dfid4  5594  fconstmpt  5762  xpundi  5768  xpundir  5769  inxpOLD  5857  csbcnv  5908  cnvco  5910  resopab  6063  opabresid  6079  cnvi  6173  cnvun  6174  cnvxp  6188  cnvcnv3  6219  coundi  6278  coundir  6279  mptun  6726  fvopab6  7063  fmptsng  7202  fmptsnd  7203  cbvoprab1  7537  cbvoprab12  7539  dmoprabss  7553  mpomptx  7563  resoprab  7568  elrnmpores  7588  ov6g  7614  1st2val  8058  2nd2val  8059  dfoprab3s  8094  dfoprab3  8095  dfoprab4  8096  opabn1stprc  8099  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabbrdOLDOLD  8124  fsplit  8158  mapsncnv  8951  xpcomco  9128  marypha2lem2  9505  oemapso  9751  ttrclresv  9786  leweon  10080  r0weon  10081  compsscnv  10440  fpwwe  10715  ltrelxr  11351  ltxrlt  11360  ltxr  13178  shftidt2  15130  prdsle  17522  prdsless  17523  prdsleval  17537  dfiso2  17833  joindm  18445  meetdm  18459  gaorb  19347  efgcpbllema  19796  frgpuplem  19814  dvdsrzring  21495  pjfval2  21752  ltbval  22084  ltbwe  22085  opsrle  22088  opsrtoslem1  22102  opsrtoslem2  22103  lmfval  23261  lmbr  23287  lgsquadlem3  27444  perpln1  28736  outpasch  28781  ishpg  28785  axcontlem2  28998  wksfval  29645  wlkson  29692  pthsfval  29757  ispth  29759  dfadj2  31917  dmadjss  31919  cnvadj  31924  mpomptxf  32695  lsmsnorb2  33385  satfv0  35326  satfvsuclem1  35327  satfvsuclem2  35328  satfbrsuc  35334  satf0  35340  satf0suclem  35343  fmlasuc0  35352  fneer  36319  bj-dfmpoa  37084  bj-mpomptALT  37085  bj-brab2a1  37115  bj-imdiridlem  37151  bj-opabco  37154  opropabco  37684  cnvepres  38254  inxp2  38323  disjecxrn  38345  xrninxp  38348  xrninxp2  38349  rnxrnres  38355  rnxrncnvepres  38356  rnxrnidres  38357  dfcoss2  38369  dfcoss3  38370  cosscnv  38372  coss1cnvres  38373  coss2cnvepres  38374  1cossres  38385  dfcoels  38386  ressn2  38398  br1cosscnvxrn  38430  1cosscnvxrn  38431  coss0  38435  cossid  38436  dfssr2  38455  cmtfvalN  39166  cmtvalN  39167  cvrfval  39224  cvrval  39225  dicval2  41136  aks6d1c1p1rcl  42065  aks6d1c1rh  42082  fgraphopab  43164  fgraphxp  43165  mptssid  45149  dfnelbr2  47188  opabbrfex0d  47201  opabbrfexd  47203  upwlksfval  47858  xpsnopab  47880  mpomptx2  48059