ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2 GIF version

Theorem eleq2 2148
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem eleq2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2079 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 118 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1493 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43anbi2d 452 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐶𝑥𝐴) ↔ (𝑥 = 𝐶𝑥𝐵)))
54exbidv 1750 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2081 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2081 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73bitr4g 221 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1285   = wceq 1287  wex 1424  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eleq12  2149  eleq2i  2151  eleq2d  2154  nelneq2  2186  clelsb4  2190  dvelimdc  2244  nelne1  2341  neleq2  2351  raleqf  2554  rexeqf  2555  reueq1f  2556  rmoeq1f  2557  rabeqf  2605  clel3g  2742  clel4  2744  sbcbi2  2878  sbcel2gv  2891  sbnfc2  2977  difeq2  3101  uneq1  3136  ineq1  3183  n0i  3280  disjel  3325  exsnrex  3470  sneqr  3589  preqr1g  3595  preqr1  3597  preq12b  3599  prel12  3600  elunii  3643  eluniab  3650  ssuni  3660  elinti  3682  elintab  3684  intss1  3688  intmin  3693  intab  3702  iineq2  3732  dfiin2g  3748  breq  3824  axsep2  3935  zfauscl  3936  inuni  3968  exmidexmid  4007  exmid01  4008  exmidundif  4011  rext  4018  intid  4027  mss  4029  opth1  4039  opeqex  4052  frforeq3  4150  frirrg  4153  limeq  4180  nsuceq0g  4221  suctr  4224  snnex  4247  uniuni  4249  iunpw  4277  ordtriexmidlem  4311  ordtriexmidlem2  4312  ordtriexmid  4313  ordtri2orexmid  4314  ontr2exmid  4316  ordtri2or2exmidlem  4317  onsucelsucexmidlem  4320  onsucelsucexmid  4321  ordsucunielexmid  4322  regexmidlem1  4324  reg2exmidlema  4325  regexmid  4326  reg2exmid  4327  elirr  4332  en2lp  4345  suc11g  4348  dtruex  4350  ordsoexmid  4353  nlimsucg  4357  onintexmid  4363  reg3exmidlemwe  4369  reg3exmid  4370  peano5  4388  limom  4403  0elnn  4407  nn0eln0  4408  nnregexmid  4409  xpeq1  4427  xpeq2  4428  opthprc  4459  xp11m  4837  funopg  5015  dffo4  5412  elunirn  5508  f1oiso  5568  eusvobj2  5601  acexmidlema  5606  acexmidlemb  5607  acexmidlemab  5609  acexmidlem2  5612  mpt2eq123  5667  unielxp  5903  cnvf1o  5949  smoel  6021  tfr0dm  6043  frecabcl  6120  nnsucelsuc  6208  nntri3or  6210  nntri2  6211  nntri3  6214  nndceq  6216  nnmordi  6229  nnaordex  6240  elqsn0m  6314  qsel  6323  mapsn  6401  findcard2s  6560  undifdcss  6587  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  elni2  6820  addnidpig  6842  elinp  6980  pitonn  7332  peano1nnnn  7336  peano2nnnn  7337  peano5nnnn  7374  peano5nni  8363  1nn  8371  peano2nn  8372  dfuzi  8792  uz11  8976  elfzonlteqm1  9552  frec2uzltd  9741  0tonninf  9776  1tonninf  9777  sumeq1  10639  bdsep2  11246  bdzfauscl  11250  bj-indeq  11293  bj-nn0suc0  11314  bj-nnelirr  11317  bj-peano4  11319  bj-inf2vnlem2  11335  bj-nn0sucALT  11342  bj-findis  11343  nninfsellemdc  11371  nninfsellemqall  11376
  Copyright terms: Public domain W3C validator