Theorem epeli 5557

Description: The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5556. (Contributed by Scott Fenton, 11-Apr-2012.)

Hypothesis

Ref	Expression
epeli.1	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
epeli	⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

Proof of Theorem epeli

Step	Hyp	Ref	Expression
1		epeli.1	. 2 ⊢ 𝐵 ∈ V
2		epelg 5556	. 2 ⊢ (𝐵 ∈ V → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   class class class wbr 5106   E cep 5554

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-eprel 5555

This theorem is used by:  epel  5558  0sn0ep  5559  smoiso  8398  smoiso2  8405  ecid  8829  ordiso2  9536  cantnflt  9700  cantnfp1lem3  9708  oemapso  9710  cantnflem1b  9714  cantnflem1  9717  cantnf  9721  wemapwe  9725  cnfcomlem  9727  cnfcom  9728  cnfcom3lem  9731  leweon  10117  r0weon  10118  alephiso  10204  fin23lem27  10433  fpwwe2lem8  10750  oniso  28687  ex-eprel  31064  onf1we  35803  cardpred  35805  werankwe  35821  werankwe2  35822  j00smo  36005  maxssj0  36006  vonf1osev  36040  satefvfmla0  36350  satefvfmla1  36357  dftr6  36694  coep  36695  coepr  36696  brsset  36829  brtxpsd  36834  brcart  36872  dfrecs2  36892  dfrdg4  36893  cnambfre  38778  wepwsolem  44242  dnwech  44248  rankrelp  46145