![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrabf | Structured version Visualization version GIF version |
Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
Ref | Expression |
---|---|
elrabf.1 | ⊢ Ⅎ𝑥𝐴 |
elrabf.2 | ⊢ Ⅎ𝑥𝐵 |
elrabf.3 | ⊢ Ⅎ𝑥𝜓 |
elrabf.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
elrabf | ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3498 | . 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V) | |
2 | elex 3498 | . . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) | |
3 | 2 | adantr 480 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V) |
4 | df-rab 3433 | . . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} | |
5 | 4 | eleq2i 2830 | . . 3 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}) |
6 | elrabf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
7 | elrabf.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐵 | |
8 | 6, 7 | nfel 2917 | . . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
9 | elrabf.3 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
10 | 8, 9 | nfan 1896 | . . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 ∧ 𝜓) |
11 | eleq1 2826 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
12 | elrabf.4 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
13 | 11, 12 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
14 | 6, 10, 13 | elabgf 3674 | . . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
15 | 5, 14 | bitrid 283 | . 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))) |
16 | 1, 3, 15 | pm5.21nii 378 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 Ⅎwnf 1779 ∈ wcel 2105 {cab 2711 Ⅎwnfc 2887 {crab 3432 Vcvv 3477 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1539 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-rab 3433 df-v 3479 |
This theorem is referenced by: rabtru 3691 invdisjrab 5134 rabxfrd 5422 f1ossf1o 7147 onminsb 7813 nnawordex 8673 tskwe 9987 rabssnn0fi 14023 iundisj 25596 sltval2 27715 iundisjf 32608 iundisjfi 32803 bnj1388 35025 phpreu 37590 poimirlem26 37632 sticksstones1 42127 rfcnpre3 44970 rfcnpre4 44971 uzwo4 44992 disjinfi 45134 allbutfiinf 45369 fsumiunss 45530 fnlimfvre 45629 stoweidlem26 45981 stoweidlem27 45982 stoweidlem31 45986 stoweidlem34 45989 stoweidlem51 46006 stoweidlem52 46007 stoweidlem59 46014 fourierdlem20 46082 fourierdlem79 46140 pimdecfgtioc 46670 smfpimcclem 46762 prmdvdsfmtnof1lem1 47508 |
Copyright terms: Public domain | W3C validator |