Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elin2d Structured version   Visualization version   GIF version

Theorem elin2d 4126
 Description: Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
Hypothesis
Ref Expression
elin1d.1 (𝜑𝑋 ∈ (𝐴𝐵))
Assertion
Ref Expression
elin2d (𝜑𝑋𝐵)

Proof of Theorem elin2d
StepHypRef Expression
1 elin1d.1 . 2 (𝜑𝑋 ∈ (𝐴𝐵))
2 elinel2 4123 . 2 (𝑋 ∈ (𝐴𝐵) → 𝑋𝐵)
31, 2syl 17 1 (𝜑𝑋𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3880 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-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888 This theorem is referenced by:  f1opwfi  8815  elfiun  8881  ordtypelem3  8971  infpwfien  9476  ttukeylem6  9928  fpwwe2lem11  10055  explecnv  15215  bitsinv1  15784  smuval2  15824  firest  16701  sscres  17088  funcres2c  17166  coffth  17201  rescfth  17202  catcoppccl  17363  catcfuccl  17364  catcxpccl  17452  psssdm2  17820  frgpnabllem2  18991  sralmod  19956  zringlpirlem3  20183  mplind  20747  neiptoptop  21746  restbas  21773  ordtrest  21817  subbascn  21869  lmss  21913  cnconn  22037  clsconn  22045  conncompclo  22050  subislly  22096  cldllycmp  22110  1stckgenlem  22168  txcls  22219  txcnp  22235  txtube  22255  txcmplem1  22256  txkgen  22267  xkopt  22270  xkococnlem  22274  txconn  22304  basqtop  22326  tgqtop  22327  kqnrmlem1  22358  kqnrmlem2  22359  nrmhmph  22409  uzrest  22512  alexsubALTlem3  22664  ptcmplem2  22668  tsmslem1  22744  tsmsxplem1  22768  tsmsxplem2  22769  tsmsxp  22770  blin2  23046  met2ndci  23139  zdis  23431  reconnlem2  23442  reconn  23443  xrge0gsumle  23448  cnheibor  23570  lebnum  23579  nmoleub2lem3  23730  nmoleub3  23734  caussi  23911  minveclem4b  24045  minveclem4  24046  ovolfcl  24080  ovolfioo  24081  ovolficc  24082  ovolficcss  24083  ovolfsval  24084  ovoliunlem1  24116  ovolicc2lem4  24134  ovolicc2lem5  24135  uniiccdif  24192  uniioovol  24193  uniiccvol  24194  uniioombllem2a  24196  uniioombllem3a  24198  uniioombllem4  24200  uniioombllem5  24201  uniioombllem6  24202  vitalilem2  24223  vitalilem4  24225  ig1peu  24782  taylfvallem1  24962  tayl0  24967  ppisval  25699  chtf  25703  efchtcl  25706  chtge0  25707  ppinprm  25747  chtprm  25748  chtnprm  25749  chtwordi  25751  chtdif  25753  efchtdvds  25754  chtlepsi  25800  chtleppi  25804  pclogsum  25809  chpval2  25812  chpchtsum  25813  chpub  25814  chebbnd1lem1  26063  chtppilimlem1  26067  rplogsumlem2  26079  perpneq  26518  ragperp  26521  tocyc01  30820  cyc3evpm  30852  cycpmconjslem2  30857  cyc3conja  30859  lbsdiflsp0  31125  esum2d  31477  ispisys2  31537  sigapisys  31539  sigapildsyslem  31545  sigapildsys  31546  sseqf  31775  tgoldbachgt  32059  bnj1172  32398  mhpind  39500  cnrefiisplem  42514  hoiqssbllem3  43306  smflimlem3  43449
 Copyright terms: Public domain W3C validator