Theorem ralrn 7033

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6846	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6891	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2748	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3088	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 289	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 483	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5342	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065  Vcvv 3433  ran crn 5622   Fn wfn 6484  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  ralrnmptw  7039  ralrnmpt  7041  cbvfo  7237  isoselem  7289  indexfi  9264  ordtypelem9  9435  ordtypelem10  9436  wemapwe  9613  numacn  9966  acndom  9968  rpnnen1lem3  12924  fsequb2  13933  limsuple  15435  limsupval2  15437  climsup  15627  ruclem11  16202  ruclem12  16203  prmreclem6  16887  imasaddfnlem  17487  imasvscafn  17496  cycsubgcl  19176  ghmrn  19199  ghmnsgima  19210  pgpssslw  19584  gexex  19823  dprdfcntz  19987  znf1o  21530  frlmlbs  21776  lindfrn  21800  ptcnplem  23608  kqt0lem  23723  isr0  23724  regr1lem2  23727  uzrest  23884  tmdgsum2  24083  imasf1oxmet  24362  imasf1omet  24363  bndth  24947  evth  24948  ovolficcss  25458  ovollb2lem  25477  ovolunlem1  25486  ovoliunlem1  25491  ovoliunlem2  25492  ovoliun2  25495  ovolscalem1  25502  ovolicc1  25505  voliunlem2  25540  voliunlem3  25541  ioombl1lem4  25550  uniioovol  25568  uniioombllem2  25572  uniioombllem3  25574  uniioombllem6  25577  volsup2  25594  vitalilem3  25599  mbfsup  25653  mbfinf  25654  mbflimsup  25655  itg1ge0  25675  itg1mulc  25693  itg1climres  25703  mbfi1fseqlem4  25707  itg2seq  25731  itg2monolem1  25739  itg2mono  25742  itg2i1fseq2  25745  itg2gt0  25749  itg2cnlem1  25750  itg2cn  25752  limciun  25883  plycpn  26277  hmopidmchi  32244  hmopidmpji  32245  rge0scvg  34145  mclsax  35812  mblfinlem2  38040  ismtyhmeolem  38186  nacsfix  43176  fnwe2lem2  43511  gneispace  44593  climinf  46065  liminfval2  46225