| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elrab3 | Structured version Visualization version GIF version | ||
| Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 5-Oct-2006.) |
| Ref | Expression |
|---|---|
| elrab.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| elrab3 | ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elrab.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | elrab 3692 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
| 3 | 2 | baib 535 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {crab 3436 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 |
| This theorem is referenced by: unimax 4944 fnelfp 7195 fnelnfp 7197 fnse 8158 fin23lem30 10382 isf32lem5 10397 negn0 11692 ublbneg 12975 supminf 12977 sadval 16493 smuval 16518 dvdslcm 16635 dvdslcmf 16668 isprm2lem 16718 isacs1i 17700 isinito 18041 istermo 18042 subgacs 19179 nsgacs 19180 odngen 19595 sdrgacs 20802 lssacs 20965 mretopd 23100 txkgen 23660 xkoco1cn 23665 xkoco2cn 23666 xkoinjcn 23695 ordthmeolem 23809 shft2rab 25543 sca2rab 25547 lhop1lem 26052 ftalem5 27120 vmasum 27260 eqscut2 27851 elmade 27906 israg 28705 ebtwntg 28997 eupth2lem3lem3 30249 eupth2lem3lem4 30250 eupth2lem3lem6 30252 cycpmco2lem1 33146 cycpmco2lem4 33149 cycpmco2 33153 ssdifidllem 33484 1arithufdlem2 33573 tgoldbachgt 34678 cvmliftmolem1 35286 neibastop3 36363 fdc 37752 pclvalN 39892 dvhb1dimN 40988 hdmaplkr 41915 aks4d1p8 42088 sticksstones1 42147 fsuppssind 42603 diophren 42824 islmodfg 43081 fsovcnvlem 44026 ntrneiel 44094 radcnvrat 44333 supminfxr 45475 stoweidlem34 46049 |
| Copyright terms: Public domain | W3C validator |