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

Theorem elabg 3663
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2366. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2130, ax-11 2147, ax-12 2164. (Revised by SN, 5-Oct-2024.)
Hypothesis
Ref Expression
elabg.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elabg (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg
StepHypRef Expression
1 elab6g 3655 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ ∀𝑥(𝑥 = 𝐴𝜑)))
2 elabg.1 . . . . . 6 (𝑥 = 𝐴 → (𝜑𝜓))
32pm5.74i 271 . . . . 5 ((𝑥 = 𝐴𝜑) ↔ (𝑥 = 𝐴𝜓))
43albii 1814 . . . 4 (∀𝑥(𝑥 = 𝐴𝜑) ↔ ∀𝑥(𝑥 = 𝐴𝜓))
5 19.23v 1938 . . . 4 (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
64, 5bitri 275 . . 3 (∀𝑥(𝑥 = 𝐴𝜑) ↔ (∃𝑥 𝑥 = 𝐴𝜓))
7 elisset 2810 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
8 pm5.5 361 . . . 4 (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴𝜓) ↔ 𝜓))
97, 8syl 17 . . 3 (𝐴𝑉 → ((∃𝑥 𝑥 = 𝐴𝜓) ↔ 𝜓))
106, 9bitrid 283 . 2 (𝐴𝑉 → (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓))
111, 10bitrd 279 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1532   = wceq 1534  wex 1774  wcel 2099  {cab 2704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805
This theorem is referenced by:  elab  3665  elab2g  3667  elabd  3668  elab3g  3672  sbcieg  3814  intmin3  4974  elabrexg  7247  finds  7898  elfi  9428  inficl  9440  dffi3  9446  scott0  9901  elgch  10637  nqpr  11029  hashf1lem1  14439  hashf1lem1OLD  14440  cshword  14765  trclublem  14966  cotrtrclfv  14983  dfiso2  17746  efgcpbllemb  19701  frgpuplem  19718  lspsn  20875  mpfind  22040  pf1ind  22261  eltg  22847  eltg2  22848  islocfin  23408  fbssfi  23728  nosupres  27627  nosupbnd1lem3  27630  nosupbnd1lem5  27632  noinffv  27641  noinfres  27642  noinfbnd1lem3  27645  noinfbnd1lem5  27647  isewlk  29403  elabreximd  32291  abfmpunirn  32421  fmlafvel  34931  isfmlasuc  34934  poimirlem3  37031  poimirlem25  37053  islshpkrN  38529  sticksstones8  41557  sticksstones9  41558  sticksstones11  41560  sticksstones17  41567  sticksstones18  41568  sn-iotalem  41629  setindtrs  42368  frege55lem1c  43269  nzss  43677  afvelrnb  46466  afvelrnb0  46467  dfatco  46559  elsetpreimafvb  46647  isgrim  47089  setis  48052
  Copyright terms: Public domain W3C validator