![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexbidv2 | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
rexbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
rexbidv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | exbidv 1922 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∃wex 1779 ∈ wcel 2104 ∃wrex 3068 |
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 1911 |
This theorem depends on definitions: df-bi 206 df-ex 1780 df-rex 3069 |
This theorem is referenced by: rexbidva 3174 rexeqbidv 3341 rexss 4054 exopxfr2 5843 isoini 7337 rexsupp 8169 omabs 8652 elfi2 9411 wemapsolem 9547 ltexpi 10899 rexuz 12886 ncoprmgcdne1b 16591 lpigen 21094 llyi 23198 nllyi 23199 elpi1 24792 ressupprn 32179 xrecex 32353 bnj18eq1 34236 ldual1dim 38339 pmapjat1 39027 mrefg2 41747 islssfg2 42115 fourierdlem71 45191 hoiqssbl 45639 lubeldm2d 47678 glbeldm2d 47679 |
Copyright terms: Public domain | W3C validator |