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

Theorem elintrab 4853
 Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999.)
Hypothesis
Ref Expression
inteqab.1 𝐴 ∈ V
Assertion
Ref Expression
elintrab (𝐴 {𝑥𝐵𝜑} ↔ ∀𝑥𝐵 (𝜑𝐴𝑥))
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem elintrab
StepHypRef Expression
1 inteqab.1 . . . 4 𝐴 ∈ V
21elintab 4852 . . 3 (𝐴 {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥((𝑥𝐵𝜑) → 𝐴𝑥))
3 impexp 454 . . . 4 (((𝑥𝐵𝜑) → 𝐴𝑥) ↔ (𝑥𝐵 → (𝜑𝐴𝑥)))
43albii 1821 . . 3 (∀𝑥((𝑥𝐵𝜑) → 𝐴𝑥) ↔ ∀𝑥(𝑥𝐵 → (𝜑𝐴𝑥)))
52, 4bitri 278 . 2 (𝐴 {𝑥 ∣ (𝑥𝐵𝜑)} ↔ ∀𝑥(𝑥𝐵 → (𝜑𝐴𝑥)))
6 df-rab 3079 . . . 4 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
76inteqi 4845 . . 3 {𝑥𝐵𝜑} = {𝑥 ∣ (𝑥𝐵𝜑)}
87eleq2i 2843 . 2 (𝐴 {𝑥𝐵𝜑} ↔ 𝐴 {𝑥 ∣ (𝑥𝐵𝜑)})
9 df-ral 3075 . 2 (∀𝑥𝐵 (𝜑𝐴𝑥) ↔ ∀𝑥(𝑥𝐵 → (𝜑𝐴𝑥)))
105, 8, 93bitr4i 306 1 (𝐴 {𝑥𝐵𝜑} ↔ ∀𝑥𝐵 (𝜑𝐴𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2111  {cab 2735  ∀wral 3070  {crab 3074  Vcvv 3409  ∩ cint 4841 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-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rab 3079  df-int 4842 This theorem is referenced by:  elintrabg  4854  intmin  4861  rankunb  9317  isf34lem4  9842  ist1-3  22054  filufint  22625  elspani  29430  ldsysgenld  31651  ldgenpisyslem1  31654  kur14lem9  32696  naddelim  33427  pclclN  37493  elpclN  37494  lcosslsp  45240
 Copyright terms: Public domain W3C validator